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 414 | 1 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: iba 528 ancr 547 anc2r 555 19.29r 1866 19.40b 1880 19.41v 1941 19.41 2227 2ax6elem 2485 mo3 2641 2mo 2726 relopabi 5687 smoord 7991 fisupg 8754 winalim2 10106 relin01 11152 cshwlen 14149 aalioulem5 24852 musum 25695 chrelat2i 30069 bnj1173 32171 waj-ax 33659 hlrelat2 36419 pm11.71 40606 onfrALTlem2 40757 19.41rg 40761 not12an2impnot1 40779 onfrALTlem2VD 41100 2pm13.193VD 41114 ax6e2eqVD 41118 ssfz12 43391 |
Copyright terms: Public domain | W3C validator |