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  6814  xposdif  9986  qbtwnz  10375  seq3f1o  10643  exp3vallem  10666  fihashf1rn  10914  xrmin2inf  11498  sumrbdclem  11607  summodclem3  11610  zsumdc  11614  fsum3cvg2  11624  mertenslem2  11766  mertensabs  11767  prodrbdclem  11801  prodmodclem2a  11806  zproddc  11809  eftcl  11884  divalgmod  12157  bitsmod  12186  gcdsupex  12197  gcdsupcl  12198  cncongr2  12345  isprm3  12359  eulerthlemrprm  12470  eulerthlema  12471  pcmptdvds  12587  prdsex  13019  elplyd  15131  ply1term  15133  lgsval2lem  15405  nninfself  15814
  Copyright terms: Public domain W3C validator