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 210 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: imim21b 395 pm4.87 837 imimorb 944 sbrimvlem 2092 r19.21v 3175 r19.21t 3214 reu8 3723 unissb 4863 reusv3 5297 fun11 6422 oeordi 8203 marypha1lem 8886 aceq1 9532 pwfseqlem3 10071 prime 12052 raluz2 12286 rlimresb 14912 isprm3 16017 isprm4 16018 acsfn 16920 pgpfac1 19133 pgpfac 19137 fbfinnfr 22379 wilthlem3 25575 isch3 28946 elat2 30045 fvineqsneq 34576 wl-dfralflem 34720 isat3 36325 cdleme32fva 37455 elmapintrab 39816 ntrneik2 40322 ntrneix2 40323 ntrneikb 40324 pm10.541 40579 pm10.542 40580 |
Copyright terms: Public domain | W3C validator |