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. Its associated inference is pm3.2i 471 and its associated deduction is jca 512 (and the double deduction is jcad 513). See pm3.2im 162 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 413 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: pm3.2i 471 pm3.43i 473 jca 512 jcad 513 ancl 545 19.29 1865 19.40b 1880 sban 2077 sb1 2496 mo4 2643 axia3 2775 r19.26 3167 r19.29 3251 difrab 4274 reuss2 4280 dmcosseq 5837 fvn0fvelrn 6917 soxp 7812 suppofssd 7856 smoord 7991 xpwdomg 9037 alephexp2 9991 lediv2a 11522 ssfzo12 13118 r19.29uz 14698 gsummoncoe1 20400 fbun 22376 fisshasheq 32249 isdrngo3 35118 or3or 40249 pm11.71 40606 tratrb 40747 onfrALTlem3 40755 elex22VD 41050 en3lplem1VD 41054 tratrbVD 41072 undif3VD 41093 onfrALTlem3VD 41098 19.41rgVD 41113 2pm13.193VD 41114 ax6e2eqVD 41118 2uasbanhVD 41122 vk15.4jVD 41125 fzoopth 43404 |
Copyright terms: Public domain | W3C validator |