Theorem syl2an2r 597

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  4570  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  mapen  7015  fival  7145  supelti  7177  supmaxti  7179  infminti  7202  xnegdi  10072  frecuzrdgsuc  10644  hashunlem  11034  ccatrn  11152  swrdccat2  11211  pfxsuff1eqwrdeq  11239  ccatpfx  11241  swrdccatin2  11269  pfxccatin12lem2  11271  2zsupmax  11745  xrmin1inf  11786  serf0  11871  fsumabs  11984  binomlem  12002  cvgratz  12051  efcllemp  12177  ef0lem  12179  tannegap  12247  modm1div  12319  divalglemnqt  12439  bitsfzolem  12473  lcmid  12610  hashdvds  12751  prmdivdiv  12767  odzcllem  12773  reumodprminv  12784  nnnn0modprm0  12786  pythagtrip  12814  pcmpt  12874  pockthg  12888  4sqlem9  12917  4sqleminfi  12928  4sqexercise1  12929  4sqlem11  12932  ennnfonelemkh  12991  ctinf  13009  nninfdclemcl  13027  nninfdclemp1  13029  setsslid  13091  imasival  13347  imasaddflemg  13357  grpinvalem  13426  issubmnd  13483  imasmnd  13494  isgrpinv  13595  grpinvssd  13618  pwssub  13654  imasgrp  13656  mulgnndir  13696  subginv  13726  subginvcl  13728  ghmpreima  13811  conjnsg  13826  srgidmlem  13949  ringidmlem  13993  imasring  14035  dvdsr01  14076  unitnegcl  14102  01eq0ring  14161  issubrng2  14182  subrginv  14209  subrgunit  14211  aprsym  14256  lmodvneg1  14302  lspsn  14388  isridlrng  14454  lidl0cl  14455  rspcl  14463  rspssid  14464  rnglidlmmgm  14468  2idlcpblrng  14495  quscrng  14505  rspsn  14506  znidom  14629  psrlinv  14656  psr1clfi  14660  topbas  14749  tgrest  14851  txss12  14948  mpomulcn  15248  cnplimclemle  15350  dvconstss  15380  efltlemlt  15456  coseq0q4123  15516  lgsval  15691  lgscllem  15694  gausslemma2dlem1a  15745  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787  2lgsoddprm  15800  uspgr2wlkeq  16086  fidcen  16379  neapmkvlem  16465