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

Theorem com3l 80
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  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com3l  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )

Proof of Theorem com3l
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 78 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com3r 78 1  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
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  83  impd  251  expdcom  1376  nebidc  2335  sbcimdv  2904  prel12  3615  reusv3  4282  relcoi1  4962  oprabid  5681  poxp  5997  reldmtpos  6018  tfrlem9  6084  tfri3  6132  ordiso2  6728  distrlem5prl  7145  distrlem5pru  7146  bndndx  8672  uzind2  8858  leexp1a  10010  cncongr1  11363  bj-inf2vnlem2  11866
  Copyright terms: Public domain W3C validator