Theorem syl2an2r 595

Description: syl2anr 290 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

Ref	Expression
syl2an2r.1	⊢ (𝜑 → 𝜓)
syl2an2r.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)
syl2an2r.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl2an2r	⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Proof of Theorem syl2an2r

Step	Hyp	Ref	Expression
1		syl2an2r.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an2r.2	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
3		syl2an2r.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	1, 2, 3	syl2an 289	. 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜒)) → 𝜏)
5	4	anabss5 578	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

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:  op1stbg  4480  mapen  6846  fival  6969  supelti  7001  supmaxti  7003  infminti  7026  xnegdi  9868  frecuzrdgsuc  10414  hashunlem  10784  2zsupmax  11234  xrmin1inf  11275  serf0  11360  fsumabs  11473  binomlem  11491  cvgratz  11540  efcllemp  11666  ef0lem  11668  tannegap  11736  modm1div  11807  divalglemnqt  11925  lcmid  12080  hashdvds  12221  prmdivdiv  12237  odzcllem  12242  reumodprminv  12253  nnnn0modprm0  12255  pythagtrip  12283  pcmpt  12341  pockthg  12355  4sqlem9  12384  ennnfonelemkh  12413  ctinf  12431  nninfdclemp1  12451  setsslid  12513  imasival  12727  imasaddflemg  12737  grprinvlem  12804  issubmnd  12843  isgrpinv  12926  grpinvssd  12947  mulgnndir  13012  subginv  13041  subginvcl  13043  srgidmlem  13161  ringidmlem  13205  dvdsr01  13273  unitnegcl  13299  01eq0ring  13330  subrginv  13358  subrgunit  13360  aprsym  13374  lmodvneg1  13420  topbas  13570  tgrest  13672  txss12  13769  cnplimclemle  14140  efltlemlt  14198  coseq0q4123  14258  lgsval  14408  lgscllem  14411  neapmkvlem  14817