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  4599  caofid0l  6292  caofid0r  6293  caofid1  6294  caofid2  6295  mapen  7098  fidcen  7155  fival  7256  supelti  7292  supmaxti  7294  infminti  7317  xnegdi  10197  frecuzrdgsuc  10772  hashunlem  11163  ccatrn  11290  ccatalpha  11294  swrdccat2  11356  pfxsuff1eqwrdeq  11384  ccatpfx  11386  swrdccatin2  11414  pfxccatin12lem2  11416  2zsupmax  11904  xrmin1inf  11945  serf0  12030  fsumabs  12144  binomlem  12162  cvgratz  12211  efcllemp  12337  ef0lem  12339  tannegap  12407  modm1div  12479  divalglemnqt  12599  bitsfzolem  12633  lcmid  12770  hashdvds  12911  prmdivdiv  12927  odzcllem  12933  reumodprminv  12944  nnnn0modprm0  12946  pythagtrip  12974  pcmpt  13034  pockthg  13048  4sqlem9  13077  4sqleminfi  13088  4sqexercise1  13089  4sqlem11  13092  ennnfonelemkh  13152  ctinf  13170  nninfdclemcl  13188  nninfdclemp1  13190  setsslid  13252  imasival  13508  imasaddflemg  13518  grpinvalem  13587  issubmnd  13644  imasmnd  13655  isgrpinv  13756  grpinvssd  13779  pwssub  13815  imasgrp  13817  mulgnndir  13857  subginv  13887  subginvcl  13889  ghmpreima  13972  conjnsg  13987  gsumsplit0  14052  srgidmlem  14111  ringidmlem  14155  imasring  14197  dvdsr01  14238  unitnegcl  14264  01eq0ring  14323  issubrng2  14344  subrginv  14371  subrgunit  14373  aprsym  14419  lmodvneg1  14465  lspsn  14551  isridlrng  14617  lidl0cl  14618  rspcl  14626  rspssid  14627  rnglidlmmgm  14631  2idlcpblrng  14658  quscrng  14668  rspsn  14669  znidom  14792  psrlinv  14826  psr1clfi  14830  topbas  14919  tgrest  15021  txss12  15118  mpomulcn  15418  cnplimclemle  15520  dvconstss  15550  efltlemlt  15626  coseq0q4123  15686  lgsval  15864  lgscllem  15867  gausslemma2dlem1a  15918  lgseisen  15934  lgsquadlem1  15937  lgsquadlem2  15938  2lgslem3a1  15957  2lgslem3b1  15958  2lgslem3c1  15959  2lgslem3d1  15960  2lgsoddprm  15973  uhgrspansubgrlem  16258  uspgr2wlkeq  16347  neapmkvlem  16839