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

Theorem syl2anr 278
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
Hypotheses
Ref Expression
syl2an.1  |-  ( ph  ->  ps )
syl2an.2  |-  ( ta 
->  ch )
syl2an.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anr  |-  ( ( ta  /\  ph )  ->  th )

Proof of Theorem syl2anr
StepHypRef Expression
1 syl2an.1 . . 3  |-  ( ph  ->  ps )
2 syl2an.2 . . 3  |-  ( ta 
->  ch )
3 syl2an.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
41, 2, 3syl2an 277 . 2  |-  ( (
ph  /\  ta )  ->  th )
54ancoms 259 1  |-  ( ( ta  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  swopo  4071  opswapg  4835  coexg  4890  iotass  4912  resdif  5176  fvexg  5222  isotr  5484  xpexgALT  5788  cauappcvgprlemladdfl  6811  addgt0sr  6918  axmulass  7005  axdistr  7006  negeu  7265  ltaddnegr  7494  nnsub  8028  zltnle  8348  elz2  8370  uzaddcl  8625  qaddcl  8667  xltneg  8850  xleneg  8851  iccneg  8958  uzsubsubfz  9013  fzsplit2  9016  fzss1  9028  uzsplit  9056  fz0fzdiffz0  9089  difelfzle  9094  difelfznle  9095  fzonlt0  9125  fzouzsplit  9137  eluzgtdifelfzo  9155  elfzodifsumelfzo  9159  ssfzo12  9182  qltnle  9203  modfzo0difsn  9345  nn0ennn  9373  isermono  9401  faclbnd  9609  bcval4  9620  bcpasc  9634  crim  9686  negdvdsb  10124  dvdsnegb  10125  dvdsmul1  10129  dvdsabseq  10159  dvdsssfz1  10164  odd2np1  10184  ndvdsadd  10243  nn0seqcvgd  10263  algcvgblem  10271
  Copyright terms: Public domain W3C validator