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

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

Proof of Theorem syl2an2
StepHypRef Expression
1 syl2an2.1 . . 3  |-  ( ph  ->  ps )
2 syl2an2.2 . . 3  |-  ( ( ch  /\  ph )  ->  th )
3 syl2an2.3 . . 3  |-  ( ( ps  /\  th )  ->  ta )
41, 2, 3syl2an 289 . 2  |-  ( (
ph  /\  ( ch  /\ 
ph ) )  ->  ta )
54anabss7 583 1  |-  ( ( ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mapsnf1o  6736  xposdif  9881  qbtwnz  10251  seq3f1o  10503  exp3vallem  10520  fihashf1rn  10767  xrmin2inf  11275  sumrbdclem  11384  summodclem3  11387  zsumdc  11391  fsum3cvg2  11401  mertenslem2  11543  mertensabs  11544  prodrbdclem  11578  prodmodclem2a  11583  zproddc  11586  eftcl  11661  divalgmod  11931  gcdsupex  11957  gcdsupcl  11958  cncongr2  12103  isprm3  12117  eulerthlemrprm  12228  eulerthlema  12229  pcmptdvds  12342  prdsex  12717  lgsval2lem  14381  nninfself  14732
  Copyright terms: Public domain W3C validator