# Difference between P -\> Q and P /\\ Q

**URL:** <https://discourse.rocq-prover.org/t/difference-between-p-q-and-p-q/1519>\
**Category:** Using Rocq\
**Created:** [January 10, 2022, 11:47am UTC](https://discourse.rocq-prover.org/t/difference-between-p-q-and-p-q/1519 "2022-01-10T11:47:11Z")\
**Posts on this page:** 1\
**Showing post:** 4

<div class="post-metadata">

**Author:** ![ishanpm](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ishanpm/32/634_2.png) [@ishanpm](https://discourse.rocq-prover.org/u/ishanpm)\
**Post date:** [January 13, 2022, 12:52am UTC](https://discourse.rocq-prover.org/t/difference-between-p-q-and-p-q/1519/4 "2022-01-13T00:52:22Z")

</div>

P → Q and P /\ Q in general make very different statements. P → Q means “if P, then Q” while P /\ Q means “P and Q”. It just happens that (P /\ Q) → R and P → (Q → R) are equivalent.

You usually use “forall” with → and “exists” with /\. If you think about what those statements would actually mean, it might make it clearer:

- `forall x:T, P x -> Q x` reads as “For all x, if P x is true, then so is Q x.”
- `exists x:T, P x /\ Q x` reads as “There is some x for which P x is true, and Q x is also true.”

---

_[View the full topic](https://discourse.rocq-prover.org/t/difference-between-p-q-and-p-q/1519)._