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  4574  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  mapen  7027  fidcen  7083  fival  7163  supelti  7195  supmaxti  7197  infminti  7220  xnegdi  10096  frecuzrdgsuc  10669  hashunlem  11060  ccatrn  11179  ccatalpha  11183  swrdccat2  11245  pfxsuff1eqwrdeq  11273  ccatpfx  11275  swrdccatin2  11303  pfxccatin12lem2  11305  2zsupmax  11780  xrmin1inf  11821  serf0  11906  fsumabs  12019  binomlem  12037  cvgratz  12086  efcllemp  12212  ef0lem  12214  tannegap  12282  modm1div  12354  divalglemnqt  12474  bitsfzolem  12508  lcmid  12645  hashdvds  12786  prmdivdiv  12802  odzcllem  12808  reumodprminv  12819  nnnn0modprm0  12821  pythagtrip  12849  pcmpt  12909  pockthg  12923  4sqlem9  12952  4sqleminfi  12963  4sqexercise1  12964  4sqlem11  12967  ennnfonelemkh  13026  ctinf  13044  nninfdclemcl  13062  nninfdclemp1  13064  setsslid  13126  imasival  13382  imasaddflemg  13392  grpinvalem  13461  issubmnd  13518  imasmnd  13529  isgrpinv  13630  grpinvssd  13653  pwssub  13689  imasgrp  13691  mulgnndir  13731  subginv  13761  subginvcl  13763  ghmpreima  13846  conjnsg  13861  srgidmlem  13984  ringidmlem  14028  imasring  14070  dvdsr01  14111  unitnegcl  14137  01eq0ring  14196  issubrng2  14217  subrginv  14244  subrgunit  14246  aprsym  14291  lmodvneg1  14337  lspsn  14423  isridlrng  14489  lidl0cl  14490  rspcl  14498  rspssid  14499  rnglidlmmgm  14503  2idlcpblrng  14530  quscrng  14540  rspsn  14541  znidom  14664  psrlinv  14691  psr1clfi  14695  topbas  14784  tgrest  14886  txss12  14983  mpomulcn  15283  cnplimclemle  15385  dvconstss  15415  efltlemlt  15491  coseq0q4123  15551  lgsval  15726  lgscllem  15729  gausslemma2dlem1a  15780  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  2lgsoddprm  15835  uspgr2wlkeq  16176  neapmkvlem  16621