Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bi2.04 | GIF version |
Description: Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bi2.04 | ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.04 76 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | |
2 | pm2.04 76 | . 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) | |
3 | 1, 2 | impbii 117 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: imim21b 241 pm4.87 493 imimorbdc 795 sbcom2v 1861 mor 1942 r19.21t 2394 reu8 2737 ra5 2846 unissb 3610 reusv3 4192 zfregfr 4298 tfi 4305 fun11 4966 prime 8337 raluz2 8522 bj-inf2vnlem2 10096 |
Copyright terms: Public domain | W3C validator |