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  3imp231  1179  expdcom  1422  nebidc  2407  sbcimdv  3002  prel12  3734  reusv3  4420  relcoi1  5117  oprabid  5853  poxp  6179  reldmtpos  6200  tfrlem9  6266  tfri3  6314  ordiso2  6979  distrlem5prl  7506  distrlem5pru  7507  bndndx  9089  uzind2  9276  leexp1a  10474  cncongr1  11980  bj-inf2vnlem2  13557
  Copyright terms: Public domain W3C validator