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  4570  caofid0l  6245  caofid0r  6246  caofid1  6247  caofid2  6248  mapen  7007  fival  7137  supelti  7169  supmaxti  7171  infminti  7194  xnegdi  10064  frecuzrdgsuc  10636  hashunlem  11026  ccatrn  11144  swrdccat2  11203  pfxsuff1eqwrdeq  11231  ccatpfx  11233  swrdccatin2  11261  pfxccatin12lem2  11263  2zsupmax  11737  xrmin1inf  11778  serf0  11863  fsumabs  11976  binomlem  11994  cvgratz  12043  efcllemp  12169  ef0lem  12171  tannegap  12239  modm1div  12311  divalglemnqt  12431  bitsfzolem  12465  lcmid  12602  hashdvds  12743  prmdivdiv  12759  odzcllem  12765  reumodprminv  12776  nnnn0modprm0  12778  pythagtrip  12806  pcmpt  12866  pockthg  12880  4sqlem9  12909  4sqleminfi  12920  4sqexercise1  12921  4sqlem11  12924  ennnfonelemkh  12983  ctinf  13001  nninfdclemcl  13019  nninfdclemp1  13021  setsslid  13083  imasival  13339  imasaddflemg  13349  grpinvalem  13418  issubmnd  13475  imasmnd  13486  isgrpinv  13587  grpinvssd  13610  pwssub  13646  imasgrp  13648  mulgnndir  13688  subginv  13718  subginvcl  13720  ghmpreima  13803  conjnsg  13818  srgidmlem  13941  ringidmlem  13985  imasring  14027  dvdsr01  14068  unitnegcl  14094  01eq0ring  14153  issubrng2  14174  subrginv  14201  subrgunit  14203  aprsym  14248  lmodvneg1  14294  lspsn  14380  isridlrng  14446  lidl0cl  14447  rspcl  14455  rspssid  14456  rnglidlmmgm  14460  2idlcpblrng  14487  quscrng  14497  rspsn  14498  znidom  14621  psrlinv  14648  psr1clfi  14652  topbas  14741  tgrest  14843  txss12  14940  mpomulcn  15240  cnplimclemle  15342  dvconstss  15372  efltlemlt  15448  coseq0q4123  15508  lgsval  15683  lgscllem  15686  gausslemma2dlem1a  15737  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2lgsoddprm  15792  uspgr2wlkeq  16076  neapmkvlem  16435