![]() |
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 208 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: imim21b 394 pm4.87 842 imimorb 949 sbrimvw 2087 sbrim 2294 ralcom3 3094 r19.21vOLD 3177 r19.21t 3247 elabgtOLD 3661 reu8 3728 unissb 4942 unissbOLD 4943 reusv3 5405 fun11 6627 xpord3inddlem 8159 oeordi 8608 marypha1lem 9457 aceq1 10141 pwfseqlem3 10684 prime 12674 raluz2 12912 rlimresb 15542 isprm3 16654 isprm4 16655 acsfn 17639 pgpfac1 20037 pgpfac 20041 isdomn5 21249 fbfinnfr 23758 wilthlem3 27015 isch3 31064 elat2 32163 fvineqsneq 36891 isat3 38779 cdleme32fva 39910 elmapintrab 43006 ntrneik2 43522 ntrneix2 43523 ntrneikb 43524 pm10.541 43804 pm10.542 43805 |
Copyright terms: Public domain | W3C validator |