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  4578  caofid0l  6267  caofid0r  6268  caofid1  6269  caofid2  6270  mapen  7037  fidcen  7093  fival  7174  supelti  7206  supmaxti  7208  infminti  7231  xnegdi  10108  frecuzrdgsuc  10682  hashunlem  11073  ccatrn  11195  ccatalpha  11199  swrdccat2  11261  pfxsuff1eqwrdeq  11289  ccatpfx  11291  swrdccatin2  11319  pfxccatin12lem2  11321  2zsupmax  11809  xrmin1inf  11850  serf0  11935  fsumabs  12049  binomlem  12067  cvgratz  12116  efcllemp  12242  ef0lem  12244  tannegap  12312  modm1div  12384  divalglemnqt  12504  bitsfzolem  12538  lcmid  12675  hashdvds  12816  prmdivdiv  12832  odzcllem  12838  reumodprminv  12849  nnnn0modprm0  12851  pythagtrip  12879  pcmpt  12939  pockthg  12953  4sqlem9  12982  4sqleminfi  12993  4sqexercise1  12994  4sqlem11  12997  ennnfonelemkh  13056  ctinf  13074  nninfdclemcl  13092  nninfdclemp1  13094  setsslid  13156  imasival  13412  imasaddflemg  13422  grpinvalem  13491  issubmnd  13548  imasmnd  13559  isgrpinv  13660  grpinvssd  13683  pwssub  13719  imasgrp  13721  mulgnndir  13761  subginv  13791  subginvcl  13793  ghmpreima  13876  conjnsg  13891  gsumsplit0  13956  srgidmlem  14015  ringidmlem  14059  imasring  14101  dvdsr01  14142  unitnegcl  14168  01eq0ring  14227  issubrng2  14248  subrginv  14275  subrgunit  14277  aprsym  14322  lmodvneg1  14368  lspsn  14454  isridlrng  14520  lidl0cl  14521  rspcl  14529  rspssid  14530  rnglidlmmgm  14534  2idlcpblrng  14561  quscrng  14571  rspsn  14572  znidom  14695  psrlinv  14727  psr1clfi  14731  topbas  14820  tgrest  14922  txss12  15019  mpomulcn  15319  cnplimclemle  15421  dvconstss  15451  efltlemlt  15527  coseq0q4123  15587  lgsval  15762  lgscllem  15765  gausslemma2dlem1a  15816  lgseisen  15832  lgsquadlem1  15835  lgsquadlem2  15836  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  2lgsoddprm  15871  uhgrspansubgrlem  16156  uspgr2wlkeq  16245  neapmkvlem  16739