![]() |
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 464 and its associated deduction is jca 509 (and the double deduction is jcad 510). See pm3.2im 159 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 403 | 1 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: pm3.2i 464 pm3.43i 466 jca 509 jcad 510 ibar 526 ancl 542 19.29 1978 19.40b 1992 19.42-1OLD 2281 axia3 2790 r19.26 3274 r19.29 3282 difrab 4130 reuss2 4136 dmcosseq 5620 fvn0fvelrn 6681 soxp 7554 smoord 7728 xpwdomg 8759 alephexp2 9718 lediv2a 11247 ssfzo12 12856 r19.29uz 14467 gsummoncoe1 20034 fbun 22014 isdrngo3 34300 pm5.31r 34933 or3or 39159 pm11.71 39437 tratrb 39580 onfrALTlem3 39588 elex22VD 39893 en3lplem1VD 39897 tratrbVD 39915 undif3VD 39936 onfrALTlem3VD 39941 19.41rgVD 39956 2pm13.193VD 39957 ax6e2eqVD 39961 2uasbanhVD 39965 vk15.4jVD 39968 fzoopth 42225 |
Copyright terms: Public domain | W3C validator |