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

Theorem syl2an2 589
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 578 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  6711  xposdif  9826  qbtwnz  10195  seq3f1o  10447  exp3vallem  10464  fihashf1rn  10710  xrmin2inf  11218  sumrbdclem  11327  summodclem3  11330  zsumdc  11334  fsum3cvg2  11344  mertenslem2  11486  mertensabs  11487  prodrbdclem  11521  prodmodclem2a  11526  zproddc  11529  eftcl  11604  divalgmod  11873  gcdsupex  11899  gcdsupcl  11900  cncongr2  12045  isprm3  12059  eulerthlemrprm  12170  eulerthlema  12171  pcmptdvds  12284  lgsval2lem  13664  nninfself  14006
  Copyright terms: Public domain W3C validator