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

Theorem syl2an2r 584
Description: syl2anr 288 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2r.1  |-  ( ph  ->  ps )
syl2an2r.2  |-  ( (
ph  /\  ch )  ->  th )
syl2an2r.3  |-  ( ( ps  /\  th )  ->  ta )
Assertion
Ref Expression
syl2an2r  |-  ( (
ph  /\  ch )  ->  ta )

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.1 . . 3  |-  ( ph  ->  ps )
2 syl2an2r.2 . . 3  |-  ( (
ph  /\  ch )  ->  th )
3 syl2an2r.3 . . 3  |-  ( ( ps  /\  th )  ->  ta )
41, 2, 3syl2an 287 . 2  |-  ( (
ph  /\  ( ph  /\ 
ch ) )  ->  ta )
54anabss5 567 1  |-  ( (
ph  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  op1stbg  4400  mapen  6740  fival  6858  supelti  6889  supmaxti  6891  infminti  6914  xnegdi  9658  frecuzrdgsuc  10194  hashunlem  10557  2zsupmax  11004  xrmin1inf  11043  serf0  11128  fsumabs  11241  binomlem  11259  cvgratz  11308  efcllemp  11371  ef0lem  11373  tannegap  11442  divalglemnqt  11624  lcmid  11768  hashdvds  11904  ennnfonelemkh  11932  ctinf  11950  setsslid  12019  topbas  12246  tgrest  12348  txss12  12445  cnplimclemle  12816  coseq0q4123  12925
  Copyright terms: Public domain W3C validator