Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  com3l GIF version

Theorem com3l 81
 Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com3l (𝜓 → (𝜒 → (𝜑𝜃)))

Proof of Theorem com3l
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 79 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com3r 79 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  84  impd  252  expdcom  1401  nebidc  2362  sbcimdv  2942  prel12  3664  reusv3  4341  relcoi1  5028  oprabid  5757  poxp  6083  reldmtpos  6104  tfrlem9  6170  tfri3  6218  ordiso2  6872  distrlem5prl  7342  distrlem5pru  7343  bndndx  8880  uzind2  9067  leexp1a  10241  cncongr1  11630  bj-inf2vnlem2  12861
 Copyright terms: Public domain W3C validator