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  6823  xposdif  10003  qbtwnz  10392  seq3f1o  10660  exp3vallem  10683  fihashf1rn  10931  fun2dmnop0  10990  xrmin2inf  11521  sumrbdclem  11630  summodclem3  11633  zsumdc  11637  fsum3cvg2  11647  mertenslem2  11789  mertensabs  11790  prodrbdclem  11824  prodmodclem2a  11829  zproddc  11832  eftcl  11907  divalgmod  12180  bitsmod  12209  gcdsupex  12220  gcdsupcl  12221  cncongr2  12368  isprm3  12382  eulerthlemrprm  12493  eulerthlema  12494  pcmptdvds  12610  prdsex  13043  elplyd  15155  ply1term  15157  lgsval2lem  15429  nninfself  15883
  Copyright terms: Public domain W3C validator