Theorem syl2an2r 595

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  4515  caofid0l  6166  caofid0r  6167  caofid1  6168  caofid2  6169  mapen  6916  fival  7045  supelti  7077  supmaxti  7079  infminti  7102  xnegdi  9962  frecuzrdgsuc  10525  hashunlem  10915  2zsupmax  11410  xrmin1inf  11451  serf0  11536  fsumabs  11649  binomlem  11667  cvgratz  11716  efcllemp  11842  ef0lem  11844  tannegap  11912  modm1div  11984  divalglemnqt  12104  bitsfzolem  12138  lcmid  12275  hashdvds  12416  prmdivdiv  12432  odzcllem  12438  reumodprminv  12449  nnnn0modprm0  12451  pythagtrip  12479  pcmpt  12539  pockthg  12553  4sqlem9  12582  4sqleminfi  12593  4sqexercise1  12594  4sqlem11  12597  ennnfonelemkh  12656  ctinf  12674  nninfdclemcl  12692  nninfdclemp1  12694  setsslid  12756  imasival  13010  imasaddflemg  13020  grpinvalem  13089  issubmnd  13146  imasmnd  13157  isgrpinv  13258  grpinvssd  13281  pwssub  13317  imasgrp  13319  mulgnndir  13359  subginv  13389  subginvcl  13391  ghmpreima  13474  conjnsg  13489  srgidmlem  13612  ringidmlem  13656  imasring  13698  dvdsr01  13738  unitnegcl  13764  01eq0ring  13823  issubrng2  13844  subrginv  13871  subrgunit  13873  aprsym  13918  lmodvneg1  13964  lspsn  14050  isridlrng  14116  lidl0cl  14117  rspcl  14125  rspssid  14126  rnglidlmmgm  14130  2idlcpblrng  14157  quscrng  14167  rspsn  14168  znidom  14291  psrlinv  14318  psr1clfi  14322  topbas  14411  tgrest  14513  txss12  14610  mpomulcn  14910  cnplimclemle  15012  dvconstss  15042  efltlemlt  15118  coseq0q4123  15178  lgsval  15353  lgscllem  15356  gausslemma2dlem1a  15407  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgsoddprm  15462  neapmkvlem  15824