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 73 | . 2 ⊢ (𝜒 → (𝜑 → (𝜓 → 𝜃))) |
3 | 2 | com3r 73 | 1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com4l 78 impd 242 expdcom 1331 nebidc 2285 prel12 3542 reusv3 4192 relcoi1 4849 oprabid 5537 poxp 5853 reldmtpos 5868 tfrlem9 5935 tfri3 5953 ordiso2 6357 distrlem5prl 6684 distrlem5pru 6685 bndndx 8180 uzind2 8350 leexp1a 9309 bj-inf2vnlem2 10096 |
Copyright terms: Public domain | W3C validator |