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  4627  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  mapen  7151  fidcen  7208  fival  7310  supelti  7349  supmaxti  7351  infminti  7374  xnegdi  10288  fzsplit3  10476  frecuzrdgsuc  10873  nn0sqdc  11169  hashunlem  11267  ccatrn  11400  ccatalpha  11404  swrdccat2  11466  pfxsuff1eqwrdeq  11494  ccatpfx  11496  swrdccatin2  11524  pfxccatin12lem2  11526  2zsupmax  12016  xrmin1inf  12059  serf0  12144  fsumabs  12258  binomlem  12276  cvgratz  12325  efcllemp  12451  ef0lem  12453  tannegap  12521  modm1div  12593  divalglemnqt  12713  bitsfzolem  12747  lcmid  12884  pwbdvdseulemle  12972  hashdvds  13029  prmdivdiv  13045  odzcllem  13051  reumodprminv  13062  nnnn0modprm0  13064  pythagtrip  13092  pcmpt  13152  pockthg  13166  4sqlem9  13195  4sqleminfi  13206  4sqexercise1  13207  4sqlem11  13210  ballotfilemic  13309  ballotfilemrv2  13324  ennnfonelemkh  13362  ctinf  13380  nninfdclemcl  13398  nninfdclemp1  13400  setsslid  13462  imasival  13687  imasaddflemg  13697  grpinvalem  13765  issubmnd  13815  imasmnd  13820  isgrpinv  13919  grpinvssd  13942  imasgrp  13974  mulgnndir  14014  subginv  14044  subginvcl  14046  ghmpreima  14129  conjnsg  14144  gzsumsplit0  14239  gsumconstcmn  14267  pwssub  14324  srgidmlem  14390  ringidmlem  14435  imasring  14479  dvdsr01  14521  unitnegcl  14547  01eq0ring  14606  issubrng2  14628  subrginv  14655  subrgunit  14657  aprsym  14706  lmodvneg1  14777  lspsn  14863  isridlrng  14929  lidl0cl  14930  rspcl  14938  rspssid  14939  rnglidlmmgm  14943  2idlcpblrng  14970  quscrng  14980  rspsn  14981  znidom  15102  psrlinv  15199  psr1clfi  15203  topbas  15305  tgrest  15407  txss12  15504  mpomulcn  15804  cnplimclemle  15906  dvconstss  15936  efltlemlt  16012  coseq0q4123  16073  chtqub  16308  bposlem2  16324  lgsval  16340  lgscllem  16343  gausslemma2dlem1a  16394  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  2lgsoddprm  16449  uhgrspansubgrlem  16734  uspgr2wlkeq  16823  neapmkvlem  17336