Theorem syl2an2r 603

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 584	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  4623  caofid0l  6323  caofid0r  6324  caofid1  6325  caofid2  6326  mapen  7140  fidcen  7197  fival  7298  supelti  7336  supmaxti  7338  infminti  7361  xnegdi  10253  fzsplit3  10441  frecuzrdgsuc  10834  hashunlem  11227  ccatrn  11360  ccatalpha  11364  swrdccat2  11426  pfxsuff1eqwrdeq  11454  ccatpfx  11456  swrdccatin2  11484  pfxccatin12lem2  11486  2zsupmax  11975  xrmin1inf  12016  serf0  12101  fsumabs  12215  binomlem  12233  cvgratz  12282  efcllemp  12408  ef0lem  12410  tannegap  12478  modm1div  12550  divalglemnqt  12670  bitsfzolem  12704  lcmid  12841  hashdvds  12982  prmdivdiv  12998  odzcllem  13004  reumodprminv  13015  nnnn0modprm0  13017  pythagtrip  13045  pcmpt  13105  pockthg  13119  4sqlem9  13148  4sqleminfi  13159  4sqexercise1  13160  4sqlem11  13163  ballotfilemic  13233  ballotfilemrv2  13248  ennnfonelemkh  13286  ctinf  13304  nninfdclemcl  13322  nninfdclemp1  13324  setsslid  13386  imasival  13610  imasaddflemg  13620  grpinvalem  13688  issubmnd  13738  imasmnd  13743  isgrpinv  13842  grpinvssd  13865  imasgrp  13897  mulgnndir  13937  subginv  13967  subginvcl  13969  ghmpreima  14052  conjnsg  14067  gzsumsplit0  14131  gsumconstcmn  14149  pwssub  14199  srgidmlem  14265  ringidmlem  14310  imasring  14352  dvdsr01  14394  unitnegcl  14420  01eq0ring  14479  issubrng2  14501  subrginv  14528  subrgunit  14530  aprsym  14579  lmodvneg1  14650  lspsn  14736  isridlrng  14802  lidl0cl  14803  rspcl  14811  rspssid  14812  rnglidlmmgm  14816  2idlcpblrng  14843  quscrng  14853  rspsn  14854  znidom  14975  psrlinv  15058  psr1clfi  15062  topbas  15151  tgrest  15253  txss12  15350  mpomulcn  15650  cnplimclemle  15752  dvconstss  15782  efltlemlt  15858  coseq0q4123  15918  lgsval  16106  lgscllem  16109  gausslemma2dlem1a  16160  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  2lgsoddprm  16215  uhgrspansubgrlem  16500  uspgr2wlkeq  16589  neapmkvlem  17091