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

Theorem com13 79
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 78 . 2  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
32com23 77 1  |-  ( ch 
->  ( ps  ->  ( 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:  com24  86  an13s  532  an31s  535  funopg  4985  f1o2ndf1  5902  brecop  6285  elfz0ubfz0  9290  elfz0fzfz0  9291  fz0fzelfz0  9292  fz0fzdiffz0  9295  fzo1fzo0n0  9346  elfzodifsumelfzo  9364  ssfzo12  9387  ssfzo12bi  9388  facwordi  9841  fihashf1rn  9890  oddnn02np1  10512  oddge22np1  10513  evennn02n  10514  evennn2n  10515  dfgcd2  10635  sqrt2irr  10773  bj-inf2vnlem2  11058
  Copyright terms: Public domain W3C validator