Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm3.2 | Structured version Visualization version GIF version |
Description: Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. See pm3.2im 157 for a version using only implication and negation. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
Ref | Expression |
---|---|
pm3.2 | ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜓)) | |
2 | 1 | ex 450 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: pm3.21 464 pm3.2i 471 pm3.43i 472 ibar 525 jca 554 jcad 555 ancl 569 pm3.2an3OLD 1241 19.29 1801 19.40b 1815 19.42-1 2104 axia3 2589 r19.26 3064 r19.29 3072 difrab 3901 reuss2 3907 dmcosseq 5387 fvn0fvelrn 6430 soxp 7290 smoord 7462 xpwdomg 8490 alephexp2 9403 lediv2a 10917 ssfzo12 12561 r19.29uz 14090 gsummoncoe1 19674 fbun 21644 isdrngo3 33758 pm5.31r 34143 or3or 38319 pm11.71 38597 tratrb 38746 onfrALTlem3 38759 elex22VD 39074 en3lplem1VD 39078 tratrbVD 39097 undif3VD 39118 onfrALTlem3VD 39123 19.41rgVD 39138 2pm13.193VD 39139 ax6e2eqVD 39143 2uasbanhVD 39147 vk15.4jVD 39150 fzoopth 41337 |
Copyright terms: Public domain | W3C validator |