![]() |
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 413 | 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 207 df-an 396 |
This theorem is referenced by: iba 527 ancr 546 anc2r 554 19.29r 1872 19.40b 1886 19.41v 1947 19.41 2233 2ax6elem 2473 mo3 2562 2mo 2646 relopabi 5835 smoord 8404 fisupg 9322 winalim2 10734 relin01 11785 cshwlen 14834 aalioulem5 26393 musum 27249 chrelat2i 32394 bnj1173 34995 waj-ax 36397 sbn1ALT 36841 hlrelat2 39386 pm11.71 44393 onfrALTlem2 44544 19.41rg 44548 not12an2impnot1 44566 onfrALTlem2VD 44887 2pm13.193VD 44901 ax6e2eqVD 44905 ssfz12 47264 |
Copyright terms: Public domain | W3C validator |