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  254  3imp231  1197  expdcom  1442  nebidc  2427  sbcimdv  3030  prel12  3773  reusv3  4462  relcoi1  5162  oprabid  5910  poxp  6236  reldmtpos  6257  tfrlem9  6323  tfri3  6371  ordiso2  7037  distrlem5prl  7588  distrlem5pru  7589  bndndx  9178  uzind2  9368  leexp1a  10578  cncongr1  12106  infpnlem1  12360  bj-inf2vnlem2  14863
  Copyright terms: Public domain W3C validator