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  4606  caofid0l  6303  caofid0r  6304  caofid1  6305  caofid2  6306  mapen  7113  fidcen  7170  fival  7271  supelti  7307  supmaxti  7309  infminti  7332  xnegdi  10224  fzsplit3  10411  frecuzrdgsuc  10804  hashunlem  11197  ccatrn  11326  ccatalpha  11330  swrdccat2  11392  pfxsuff1eqwrdeq  11420  ccatpfx  11422  swrdccatin2  11450  pfxccatin12lem2  11452  2zsupmax  11941  xrmin1inf  11982  serf0  12067  fsumabs  12181  binomlem  12199  cvgratz  12248  efcllemp  12374  ef0lem  12376  tannegap  12444  modm1div  12516  divalglemnqt  12636  bitsfzolem  12670  lcmid  12807  hashdvds  12948  prmdivdiv  12964  odzcllem  12970  reumodprminv  12981  nnnn0modprm0  12983  pythagtrip  13011  pcmpt  13071  pockthg  13085  4sqlem9  13114  4sqleminfi  13125  4sqexercise1  13126  4sqlem11  13129  ballotfilemic  13199  ballotfilemrv2  13214  ennnfonelemkh  13252  ctinf  13270  nninfdclemcl  13288  nninfdclemp1  13290  setsslid  13352  imasival  13575  imasaddflemg  13585  grpinvalem  13653  issubmnd  13708  imasmnd  13713  isgrpinv  13814  grpinvssd  13837  imasgrp  13869  mulgnndir  13909  subginv  13939  subginvcl  13941  ghmpreima  14024  conjnsg  14039  gsumsplit0  14104  pwssub  14163  srgidmlem  14226  ringidmlem  14270  imasring  14312  dvdsr01  14354  unitnegcl  14380  01eq0ring  14439  issubrng2  14461  subrginv  14488  subrgunit  14490  aprsym  14539  lmodvneg1  14609  lspsn  14695  isridlrng  14761  lidl0cl  14762  rspcl  14770  rspssid  14771  rnglidlmmgm  14775  2idlcpblrng  14802  quscrng  14812  rspsn  14813  znidom  14936  psrlinv  14970  psr1clfi  14974  topbas  15063  tgrest  15165  txss12  15262  mpomulcn  15562  cnplimclemle  15664  dvconstss  15694  efltlemlt  15770  coseq0q4123  15830  lgsval  16008  lgscllem  16011  gausslemma2dlem1a  16062  lgseisen  16078  lgsquadlem1  16081  lgsquadlem2  16082  2lgslem3a1  16101  2lgslem3b1  16102  2lgslem3c1  16103  2lgslem3d1  16104  2lgsoddprm  16117  uhgrspansubgrlem  16402  uspgr2wlkeq  16491  neapmkvlem  16993