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  4576  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  mapen  7032  fidcen  7088  fival  7169  supelti  7201  supmaxti  7203  infminti  7226  xnegdi  10103  frecuzrdgsuc  10677  hashunlem  11068  ccatrn  11187  ccatalpha  11191  swrdccat2  11253  pfxsuff1eqwrdeq  11281  ccatpfx  11283  swrdccatin2  11311  pfxccatin12lem2  11313  2zsupmax  11788  xrmin1inf  11829  serf0  11914  fsumabs  12028  binomlem  12046  cvgratz  12095  efcllemp  12221  ef0lem  12223  tannegap  12291  modm1div  12363  divalglemnqt  12483  bitsfzolem  12517  lcmid  12654  hashdvds  12795  prmdivdiv  12811  odzcllem  12817  reumodprminv  12828  nnnn0modprm0  12830  pythagtrip  12858  pcmpt  12918  pockthg  12932  4sqlem9  12961  4sqleminfi  12972  4sqexercise1  12973  4sqlem11  12976  ennnfonelemkh  13035  ctinf  13053  nninfdclemcl  13071  nninfdclemp1  13073  setsslid  13135  imasival  13391  imasaddflemg  13401  grpinvalem  13470  issubmnd  13527  imasmnd  13538  isgrpinv  13639  grpinvssd  13662  pwssub  13698  imasgrp  13700  mulgnndir  13740  subginv  13770  subginvcl  13772  ghmpreima  13855  conjnsg  13870  gsumsplit0  13935  srgidmlem  13994  ringidmlem  14038  imasring  14080  dvdsr01  14121  unitnegcl  14147  01eq0ring  14206  issubrng2  14227  subrginv  14254  subrgunit  14256  aprsym  14301  lmodvneg1  14347  lspsn  14433  isridlrng  14499  lidl0cl  14500  rspcl  14508  rspssid  14509  rnglidlmmgm  14513  2idlcpblrng  14540  quscrng  14550  rspsn  14551  znidom  14674  psrlinv  14701  psr1clfi  14705  topbas  14794  tgrest  14896  txss12  14993  mpomulcn  15293  cnplimclemle  15395  dvconstss  15425  efltlemlt  15501  coseq0q4123  15561  lgsval  15736  lgscllem  15739  gausslemma2dlem1a  15790  lgseisen  15806  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem3a1  15829  2lgslem3b1  15830  2lgslem3c1  15831  2lgslem3d1  15832  2lgsoddprm  15845  uhgrspansubgrlem  16130  uspgr2wlkeq  16219  neapmkvlem  16692