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 expdcom 1403 nebidc 2365 sbcimdv 2946 prel12 3668 reusv3 4351 relcoi1 5040 oprabid 5771 poxp 6097 reldmtpos 6118 tfrlem9 6184 tfri3 6232 ordiso2 6888 distrlem5prl 7362 distrlem5pru 7363 bndndx 8934 uzind2 9121 leexp1a 10303 cncongr1 11696 bj-inf2vnlem2 13065 |
Copyright terms: Public domain | W3C validator |