![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > com3l | GIF version |
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) |
Ref | Expression |
---|---|
com3.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
com3l | ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com3.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | com3r 79 | . 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃))) |
3 | 2 | com3r 79 | 1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com4l 84 impd 254 3imp231 1197 expdcom 1442 nebidc 2427 sbcimdv 3028 prel12 3771 reusv3 4460 relcoi1 5160 oprabid 5906 poxp 6232 reldmtpos 6253 tfrlem9 6319 tfri3 6367 ordiso2 7033 distrlem5prl 7584 distrlem5pru 7585 bndndx 9174 uzind2 9364 leexp1a 10574 cncongr1 12102 infpnlem1 12356 bj-inf2vnlem2 14693 |
Copyright terms: Public domain | W3C validator |