![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bi2.04 | Structured version Visualization version GIF version |
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.) |
Ref | Expression |
---|---|
bi2.04 | ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.04 90 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | |
2 | pm2.04 90 | . 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) | |
3 | 1, 2 | impbii 201 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: imim21b 385 pm4.87 876 imimorb 980 r19.21t 3164 r19.21v 3169 reu8 3627 unissb 4691 reusv3 5105 fun11 6196 oeordi 7934 marypha1lem 8608 aceq1 9253 pwfseqlem3 9797 prime 11786 raluz2 12019 rlimresb 14673 isprm3 15768 isprm4 15769 acsfn 16672 pgpfac1 18833 pgpfac 18837 fbfinnfr 22015 wilthlem3 25209 isch3 28653 elat2 29754 isat3 35382 cdleme32fva 36512 elmapintrab 38723 ntrneik2 39230 ntrneix2 39231 ntrneikb 39232 pm10.541 39406 pm10.542 39407 |
Copyright terms: Public domain | W3C validator |