![]() |
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 82 | . 2 ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | |
2 | pm2.04 82 | . 2 ⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → 𝜒))) | |
3 | 1, 2 | impbii 125 | 1 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imim21b 251 pm4.87 547 imimorbdc 882 sbcom2v 1961 mor 2042 r19.21t 2510 reu8 2884 ra5 3001 unissb 3774 reusv3 4389 zfregfr 4496 tfi 4504 fun11 5198 prime 9174 raluz2 9401 isprm3 11835 isprm4 11836 bj-inf2vnlem2 13340 |
Copyright terms: Public domain | W3C validator |