Theorem syl2an2r 599

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 580	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  4605  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  mapen  7112  fidcen  7169  fival  7270  supelti  7306  supmaxti  7308  infminti  7331  xnegdi  10223  fzsplit3  10410  frecuzrdgsuc  10803  hashunlem  11196  ccatrn  11325  ccatalpha  11329  swrdccat2  11391  pfxsuff1eqwrdeq  11419  ccatpfx  11421  swrdccatin2  11449  pfxccatin12lem2  11451  2zsupmax  11939  xrmin1inf  11980  serf0  12065  fsumabs  12179  binomlem  12197  cvgratz  12246  efcllemp  12372  ef0lem  12374  tannegap  12442  modm1div  12514  divalglemnqt  12634  bitsfzolem  12668  lcmid  12805  hashdvds  12946  prmdivdiv  12962  odzcllem  12968  reumodprminv  12979  nnnn0modprm0  12981  pythagtrip  13009  pcmpt  13069  pockthg  13083  4sqlem9  13112  4sqleminfi  13123  4sqexercise1  13124  4sqlem11  13127  ballotfilemic  13197  ballotfilemrv2  13212  ennnfonelemkh  13250  ctinf  13268  nninfdclemcl  13286  nninfdclemp1  13288  setsslid  13350  imasival  13573  imasaddflemg  13583  grpinvalem  13651  issubmnd  13706  imasmnd  13711  isgrpinv  13812  grpinvssd  13835  imasgrp  13867  mulgnndir  13907  subginv  13937  subginvcl  13939  ghmpreima  14022  conjnsg  14037  gsumsplit0  14102  pwssub  14161  srgidmlem  14224  ringidmlem  14268  imasring  14310  dvdsr01  14352  unitnegcl  14378  01eq0ring  14437  issubrng2  14459  subrginv  14486  subrgunit  14488  aprsym  14537  lmodvneg1  14607  lspsn  14693  isridlrng  14759  lidl0cl  14760  rspcl  14768  rspssid  14769  rnglidlmmgm  14773  2idlcpblrng  14800  quscrng  14810  rspsn  14811  znidom  14934  psrlinv  14968  psr1clfi  14972  topbas  15061  tgrest  15163  txss12  15260  mpomulcn  15560  cnplimclemle  15662  dvconstss  15692  efltlemlt  15768  coseq0q4123  15828  lgsval  16006  lgscllem  16009  gausslemma2dlem1a  16060  lgseisen  16076  lgsquadlem1  16079  lgsquadlem2  16080  2lgslem3a1  16099  2lgslem3b1  16100  2lgslem3c1  16101  2lgslem3d1  16102  2lgsoddprm  16115  uhgrspansubgrlem  16400  uspgr2wlkeq  16489  neapmkvlem  16992