ILE Home 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-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