Theorem syl2an2r 597

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 578	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  4547  caofid0l  6215  caofid0r  6216  caofid1  6217  caofid2  6218  mapen  6975  fival  7105  supelti  7137  supmaxti  7139  infminti  7162  xnegdi  10032  frecuzrdgsuc  10603  hashunlem  10993  ccatrn  11110  swrdccat2  11169  pfxsuff1eqwrdeq  11197  ccatpfx  11199  swrdccatin2  11227  pfxccatin12lem2  11229  2zsupmax  11703  xrmin1inf  11744  serf0  11829  fsumabs  11942  binomlem  11960  cvgratz  12009  efcllemp  12135  ef0lem  12137  tannegap  12205  modm1div  12277  divalglemnqt  12397  bitsfzolem  12431  lcmid  12568  hashdvds  12709  prmdivdiv  12725  odzcllem  12731  reumodprminv  12742  nnnn0modprm0  12744  pythagtrip  12772  pcmpt  12832  pockthg  12846  4sqlem9  12875  4sqleminfi  12886  4sqexercise1  12887  4sqlem11  12890  ennnfonelemkh  12949  ctinf  12967  nninfdclemcl  12985  nninfdclemp1  12987  setsslid  13049  imasival  13305  imasaddflemg  13315  grpinvalem  13384  issubmnd  13441  imasmnd  13452  isgrpinv  13553  grpinvssd  13576  pwssub  13612  imasgrp  13614  mulgnndir  13654  subginv  13684  subginvcl  13686  ghmpreima  13769  conjnsg  13784  srgidmlem  13907  ringidmlem  13951  imasring  13993  dvdsr01  14033  unitnegcl  14059  01eq0ring  14118  issubrng2  14139  subrginv  14166  subrgunit  14168  aprsym  14213  lmodvneg1  14259  lspsn  14345  isridlrng  14411  lidl0cl  14412  rspcl  14420  rspssid  14421  rnglidlmmgm  14425  2idlcpblrng  14452  quscrng  14462  rspsn  14463  znidom  14586  psrlinv  14613  psr1clfi  14617  topbas  14706  tgrest  14808  txss12  14905  mpomulcn  15205  cnplimclemle  15307  dvconstss  15337  efltlemlt  15413  coseq0q4123  15473  lgsval  15648  lgscllem  15651  gausslemma2dlem1a  15702  lgseisen  15718  lgsquadlem1  15721  lgsquadlem2  15722  2lgslem3a1  15741  2lgslem3b1  15742  2lgslem3c1  15743  2lgslem3d1  15744  2lgsoddprm  15757  neapmkvlem  16346