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

Theorem com13 80
Description: Commutation of antecedents. Swap 1st and 3rd. (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
com13  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com3r 79 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com23 78 1  |-  ( ch 
->  ( ps  ->  ( ph  ->  th ) ) )
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:  com24  87  an13s  567  an31s  570  3imp31  1196  3imp21  1198  funopg  5246  f1o2ndf1  6223  brecop  6619  fiintim  6922  elpq  9637  xnn0lenn0nn0  9852  elfz0ubfz0  10111  elfz0fzfz0  10112  fz0fzelfz0  10113  fz0fzdiffz0  10116  fzo1fzo0n0  10169  elfzodifsumelfzo  10187  ssfzo12  10210  ssfzo12bi  10211  facwordi  10704  fihashf1rn  10752  oddnn02np1  11868  oddge22np1  11869  evennn02n  11870  evennn2n  11871  dfgcd2  11998  sqrt2irr  12145  zabsle1  14067  bj-inf2vnlem2  14379
  Copyright terms: Public domain W3C validator