| 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 209 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 |
| 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 |
| This theorem is referenced by: imim21b 394 pm4.87 844 imimorb 953 sbrimvw 2091 sbrim 2304 ralcom3 3097 r19.21vOLD 3181 r19.21t 3253 elabgtOLD 3673 reu8 3739 sbccomlem 3869 unissb 4939 unissbOLD 4940 reusv3 5405 fun11 6640 xpord3inddlem 8179 oeordi 8625 marypha1lem 9473 aceq1 10157 pwfseqlem3 10700 prime 12699 raluz2 12939 rlimresb 15601 isprm3 16720 isprm4 16721 acsfn 17702 pgpfac1 20100 pgpfac 20104 isdomn5 20710 fbfinnfr 23849 wilthlem3 27113 isch3 31260 elat2 32359 fvineqsneq 37413 isat3 39308 cdleme32fva 40439 indstrd 42194 elmapintrab 43589 ntrneik2 44105 ntrneix2 44106 ntrneikb 44107 pm10.541 44386 pm10.542 44387 |
| Copyright terms: Public domain | W3C validator |