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 156 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 449 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: pm3.21 463 pm3.2i 470 pm3.43i 471 ibar 524 jca 553 jcad 554 ancl 567 pm3.2an3OLD 1234 19.29 1789 19.40b 1804 19.42-1 2091 axia3 2577 r19.26 3046 r19.29 3054 difrab 3860 reuss2 3866 dmcosseq 5308 fvn0fvelrn 6335 soxp 7177 smoord 7349 xpwdomg 8373 alephexp2 9282 lediv2a 10796 ssfzo12 12427 r19.29uz 13938 gsummoncoe1 19495 fbun 21454 wlkdvspthlem 26137 usgra2adedgspthlem2 26140 usgrcyclnl2 26169 erclwwlkeqlen 26340 eupatrl 26495 isdrngo3 32928 pm5.31r 33159 or3or 37339 pm11.71 37619 tratrb 37767 onfrALTlem3 37780 elex22VD 38096 en3lplem1VD 38100 tratrbVD 38119 undif3VD 38140 onfrALTlem3VD 38145 19.41rgVD 38160 2pm13.193VD 38161 ax6e2eqVD 38165 2uasbanhVD 38169 vk15.4jVD 38172 fzoopth 40360 |
Copyright terms: Public domain | W3C validator |