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

Theorem syl2an2 566
Description: syl2an 285 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2.1 (𝜑𝜓)
syl2an2.2 ((𝜒𝜑) → 𝜃)
syl2an2.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2 ((𝜒𝜑) → 𝜏)

Proof of Theorem syl2an2
StepHypRef Expression
1 syl2an2.1 . . 3 (𝜑𝜓)
2 syl2an2.2 . . 3 ((𝜒𝜑) → 𝜃)
3 syl2an2.3 . . 3 ((𝜓𝜃) → 𝜏)
41, 2, 3syl2an 285 . 2 ((𝜑 ∧ (𝜒𝜑)) → 𝜏)
54anabss7 555 1 ((𝜒𝜑) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mapsnf1o  6583  xposdif  9552  qbtwnz  9916  seq3f1o  10164  exp3vallem  10181  fihashf1rn  10422  xrmin2inf  10923  sumrbdclem  11031  summodclem3  11035  zsumdc  11039  fsum3cvg2  11049  mertenslem2  11191  mertensabs  11192  eftcl  11205  divalgmod  11466  gcdsupex  11488  gcdsupcl  11489  cncongr2  11625  isprm3  11639  nninfself  12890
  Copyright terms: Public domain W3C validator