Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm3.21 | Structured version Visualization version GIF version |
Description: Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
pm3.21 | ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜑)) | |
2 | 1 | expcom 417 | 1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: iba 531 ancr 550 anc2r 558 19.29r 1882 19.40b 1896 19.41v 1958 19.41 2233 2ax6elem 2469 mo3 2563 2mo 2649 relopabi 5692 smoord 8102 fisupg 8919 winalim2 10310 relin01 11356 cshwlen 14364 aalioulem5 25229 musum 26073 chrelat2i 30446 bnj1173 32695 waj-ax 34340 sbn1ALT 34779 hlrelat2 37154 pm11.71 41688 onfrALTlem2 41839 19.41rg 41843 not12an2impnot1 41861 onfrALTlem2VD 42182 2pm13.193VD 42196 ax6e2eqVD 42200 ssfz12 44479 |
Copyright terms: Public domain | W3C validator |