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  6737  xposdif  9882  qbtwnz  10252  seq3f1o  10504  exp3vallem  10521  fihashf1rn  10768  xrmin2inf  11276  sumrbdclem  11385  summodclem3  11388  zsumdc  11392  fsum3cvg2  11402  mertenslem2  11544  mertensabs  11545  prodrbdclem  11579  prodmodclem2a  11584  zproddc  11587  eftcl  11662  divalgmod  11932  gcdsupex  11958  gcdsupcl  11959  cncongr2  12104  isprm3  12118  eulerthlemrprm  12229  eulerthlema  12230  pcmptdvds  12343  prdsex  12718  lgsval2lem  14414  nninfself  14765
  Copyright terms: Public domain W3C validator