![]() |
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 3030 prel12 3773 reusv3 4462 relcoi1 5162 oprabid 5910 poxp 6236 reldmtpos 6257 tfrlem9 6323 tfri3 6371 ordiso2 7037 distrlem5prl 7588 distrlem5pru 7589 bndndx 9178 uzind2 9368 leexp1a 10578 cncongr1 12106 infpnlem1 12360 bj-inf2vnlem2 14863 |
Copyright terms: Public domain | W3C validator |