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 252 3imp231 1179 expdcom 1422 nebidc 2407 sbcimdv 3002 prel12 3734 reusv3 4420 relcoi1 5117 oprabid 5853 poxp 6179 reldmtpos 6200 tfrlem9 6266 tfri3 6314 ordiso2 6979 distrlem5prl 7506 distrlem5pru 7507 bndndx 9089 uzind2 9276 leexp1a 10474 cncongr1 11980 bj-inf2vnlem2 13557 |
Copyright terms: Public domain | W3C validator |