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  4602  caofid0l  6295  caofid0r  6296  caofid1  6297  caofid2  6298  mapen  7101  fidcen  7158  fival  7259  supelti  7295  supmaxti  7297  infminti  7320  xnegdi  10207  frecuzrdgsuc  10783  hashunlem  11176  ccatrn  11305  ccatalpha  11309  swrdccat2  11371  pfxsuff1eqwrdeq  11399  ccatpfx  11401  swrdccatin2  11429  pfxccatin12lem2  11431  2zsupmax  11919  xrmin1inf  11960  serf0  12045  fsumabs  12159  binomlem  12177  cvgratz  12226  efcllemp  12352  ef0lem  12354  tannegap  12422  modm1div  12494  divalglemnqt  12614  bitsfzolem  12648  lcmid  12785  hashdvds  12926  prmdivdiv  12942  odzcllem  12948  reumodprminv  12959  nnnn0modprm0  12961  pythagtrip  12989  pcmpt  13049  pockthg  13063  4sqlem9  13092  4sqleminfi  13103  4sqexercise1  13104  4sqlem11  13107  ennnfonelemkh  13184  ctinf  13202  nninfdclemcl  13220  nninfdclemp1  13222  setsslid  13284  imasival  13540  imasaddflemg  13550  grpinvalem  13619  issubmnd  13676  imasmnd  13687  isgrpinv  13788  grpinvssd  13811  pwssub  13847  imasgrp  13849  mulgnndir  13889  subginv  13919  subginvcl  13921  ghmpreima  14004  conjnsg  14019  gsumsplit0  14084  srgidmlem  14143  ringidmlem  14187  imasring  14229  dvdsr01  14271  unitnegcl  14297  01eq0ring  14356  issubrng2  14378  subrginv  14405  subrgunit  14407  aprsym  14456  lmodvneg1  14527  lspsn  14613  isridlrng  14679  lidl0cl  14680  rspcl  14688  rspssid  14689  rnglidlmmgm  14693  2idlcpblrng  14720  quscrng  14730  rspsn  14731  znidom  14854  psrlinv  14888  psr1clfi  14892  topbas  14981  tgrest  15083  txss12  15180  mpomulcn  15480  cnplimclemle  15582  dvconstss  15612  efltlemlt  15688  coseq0q4123  15748  lgsval  15926  lgscllem  15929  gausslemma2dlem1a  15980  lgseisen  15996  lgsquadlem1  15999  lgsquadlem2  16000  2lgslem3a1  16019  2lgslem3b1  16020  2lgslem3c1  16021  2lgslem3d1  16022  2lgsoddprm  16035  uhgrspansubgrlem  16320  uspgr2wlkeq  16409  neapmkvlem  16902