![]() |
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 199 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: imim21b 381 pm4.87 607 imimorb 939 r19.21t 2984 r19.21v 2989 reu8 3435 unissb 4501 reusv3 4906 fun11 6001 oeordi 7712 marypha1lem 8380 aceq1 8978 pwfseqlem3 9520 prime 11496 raluz2 11775 rlimresb 14340 isprm3 15443 isprm4 15444 acsfn 16367 pgpfac1 18525 pgpfac 18529 fbfinnfr 21692 wilthlem3 24841 isch3 28226 elat2 29327 isat3 34912 cdleme32fva 36042 elmapintrab 38199 ntrneik2 38707 ntrneix2 38708 ntrneikb 38709 pm10.541 38883 pm10.542 38884 |
Copyright terms: Public domain | W3C validator |