| 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 1874 19.40b 1888 19.41v 1949 19.41 2235 2ax6elem 2475 mo3 2564 2mo 2648 relopabi 5832 smoord 8405 fisupg 9324 winalim2 10736 relin01 11787 cshwlen 14837 aalioulem5 26378 musum 27234 chrelat2i 32384 bnj1173 35016 waj-ax 36415 sbn1ALT 36859 hlrelat2 39405 pm11.71 44416 onfrALTlem2 44566 19.41rg 44570 not12an2impnot1 44588 onfrALTlem2VD 44909 2pm13.193VD 44923 ax6e2eqVD 44927 ssfz12 47326 |
| Copyright terms: Public domain | W3C validator |