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

Theorem com34 82
Description: Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com34  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )

Proof of Theorem com34
StepHypRef Expression
1 com4.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
2 pm2.04 81 . 2  |-  ( ( ch  ->  ( th  ->  ta ) )  -> 
( th  ->  ( ch  ->  ta ) ) )
31, 2syl6 33 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ( ch  ->  ta ) ) ) )
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  com35  89  3an1rs  1155  rspct  2715  po2nr  4136  funssres  5056  f1ocnv2d  5848  tfrlem9  6084  nnmass  6248  nnmordi  6273  genpcdl  7076  genpcuu  7077  mulnqprl  7125  mulnqpru  7126  distrlem1prl  7139  distrlem1pru  7140  divgt0  8331  divge0  8332  uzind2  8856  facdiv  10142  dvdsabseq  11122  divgcdcoprm0  11357
  Copyright terms: Public domain W3C validator