Theorem syl2an2r 603

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 584	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  op1stbg  4625  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  mapen  7146  fidcen  7203  fival  7304  supelti  7342  supmaxti  7344  infminti  7367  xnegdi  10272  fzsplit3  10460  frecuzrdgsuc  10853  hashunlem  11246  ccatrn  11379  ccatalpha  11383  swrdccat2  11445  pfxsuff1eqwrdeq  11473  ccatpfx  11475  swrdccatin2  11503  pfxccatin12lem2  11505  2zsupmax  11994  xrmin1inf  12035  serf0  12120  fsumabs  12234  binomlem  12252  cvgratz  12301  efcllemp  12427  ef0lem  12429  tannegap  12497  modm1div  12569  divalglemnqt  12689  bitsfzolem  12723  lcmid  12860  hashdvds  13001  prmdivdiv  13017  odzcllem  13023  reumodprminv  13034  nnnn0modprm0  13036  pythagtrip  13064  pcmpt  13124  pockthg  13138  4sqlem9  13167  4sqleminfi  13178  4sqexercise1  13179  4sqlem11  13182  ballotfilemic  13252  ballotfilemrv2  13267  ennnfonelemkh  13305  ctinf  13323  nninfdclemcl  13341  nninfdclemp1  13343  setsslid  13405  imasival  13629  imasaddflemg  13639  grpinvalem  13707  issubmnd  13757  imasmnd  13762  isgrpinv  13861  grpinvssd  13884  imasgrp  13916  mulgnndir  13956  subginv  13986  subginvcl  13988  ghmpreima  14071  conjnsg  14086  gzsumsplit0  14150  gsumconstcmn  14168  pwssub  14218  srgidmlem  14284  ringidmlem  14329  imasring  14371  dvdsr01  14413  unitnegcl  14439  01eq0ring  14498  issubrng2  14520  subrginv  14547  subrgunit  14549  aprsym  14598  lmodvneg1  14669  lspsn  14755  isridlrng  14821  lidl0cl  14822  rspcl  14830  rspssid  14831  rnglidlmmgm  14835  2idlcpblrng  14862  quscrng  14872  rspsn  14873  znidom  14994  psrlinv  15077  psr1clfi  15081  topbas  15170  tgrest  15272  txss12  15369  mpomulcn  15669  cnplimclemle  15771  dvconstss  15801  efltlemlt  15877  coseq0q4123  15938  lgsval  16135  lgscllem  16138  gausslemma2dlem1a  16189  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  2lgsoddprm  16244  uhgrspansubgrlem  16529  uspgr2wlkeq  16618  neapmkvlem  17129