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  1151  rspct  2695  po2nr  4072  funssres  4972  f1ocnv2d  5735  tfrlem9  5968  nnmass  6131  nnmordi  6155  genpcdl  6771  genpcuu  6772  mulnqprl  6820  mulnqpru  6821  distrlem1prl  6834  distrlem1pru  6835  divgt0  8017  divge0  8018  uzind2  8540  facdiv  9762  dvdsabseq  10392  divgcdcoprm0  10627
  Copyright terms: Public domain W3C validator