![]() |
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 470 and its associated deduction is jca 511 (and the double deduction is jcad 512). See pm3.2im 160 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 412 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 206 df-an 396 |
This theorem is referenced by: pm3.2i 470 pm3.43i 472 jca 511 jcad 512 ancl 544 19.29 1868 19.40b 1883 sban 2075 sb1 2469 mo4 2552 axia3 2682 r19.26 3103 r19.29OLD 3107 difrab 4300 reuss2 4307 dmcosseq 5962 fvn0fvelrnOLD 7153 soxp 8109 suppofssd 8183 smoord 8360 xpwdomg 9576 alephexp2 10572 lediv2a 12105 ssfzo12 13722 r19.29uz 15294 gsummoncoe1 22149 fbun 23666 fisshasheq 34593 isdrngo3 37317 cantnf2 42564 or3or 43263 pm11.71 43645 tratrb 43786 onfrALTlem3 43794 elex22VD 44089 en3lplem1VD 44093 tratrbVD 44111 undif3VD 44132 onfrALTlem3VD 44137 19.41rgVD 44152 2pm13.193VD 44153 ax6e2eqVD 44157 2uasbanhVD 44161 vk15.4jVD 44164 fzoopth 46520 |
Copyright terms: Public domain | W3C validator |