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

Theorem syl2an2 583
 Description: syl2an 287 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 287 . 2 ((𝜑 ∧ (𝜒𝜑)) → 𝜏)
54anabss7 572 1 ((𝜒𝜑) → 𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  mapsnf1o  6631  xposdif  9679  qbtwnz  10043  seq3f1o  10291  exp3vallem  10308  fihashf1rn  10549  xrmin2inf  11051  sumrbdclem  11160  summodclem3  11163  zsumdc  11167  fsum3cvg2  11177  mertenslem2  11319  mertensabs  11320  prodrbdclem  11354  prodmodclem2a  11359  eftcl  11374  divalgmod  11637  gcdsupex  11659  gcdsupcl  11660  cncongr2  11798  isprm3  11812  nninfself  13318
 Copyright terms: Public domain W3C validator