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 | pm3.2 462 | . 2 ⊢ (𝜓 → (𝜑 → (𝜓 ∧ 𝜑))) | |
2 | 1 | com12 32 | 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.22 464 iba 523 ancr 570 anc2r 577 pm5.31 610 exan 1775 exanOLD 1776 19.29r 1790 19.40b 1804 19.41v 1901 19.41 2090 2ax6elem 2437 mo3 2495 2mo 2539 relopabi 5167 smoord 7349 fisupg 8093 fiinfg 8288 winalim2 9397 relin01 10431 cshwlen 13396 aalioulem5 23895 musum 24717 chrelat2i 28608 bnj1173 30324 waj-ax 31583 hlrelat2 33707 pm11.71 37619 onfrALTlem2 37782 19.41rg 37787 not12an2impnot1 37805 onfrALTlem2VD 38147 2pm13.193VD 38161 ax6e2eqVD 38165 ssfz12 40351 |
Copyright terms: Public domain | W3C validator |