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  4530  caofid0l  6192  caofid0r  6193  caofid1  6194  caofid2  6195  mapen  6950  fival  7079  supelti  7111  supmaxti  7113  infminti  7136  xnegdi  9997  frecuzrdgsuc  10566  hashunlem  10956  ccatrn  11073  swrdccat2  11132  pfxsuff1eqwrdeq  11158  ccatpfx  11160  2zsupmax  11581  xrmin1inf  11622  serf0  11707  fsumabs  11820  binomlem  11838  cvgratz  11887  efcllemp  12013  ef0lem  12015  tannegap  12083  modm1div  12155  divalglemnqt  12275  bitsfzolem  12309  lcmid  12446  hashdvds  12587  prmdivdiv  12603  odzcllem  12609  reumodprminv  12620  nnnn0modprm0  12622  pythagtrip  12650  pcmpt  12710  pockthg  12724  4sqlem9  12753  4sqleminfi  12764  4sqexercise1  12765  4sqlem11  12768  ennnfonelemkh  12827  ctinf  12845  nninfdclemcl  12863  nninfdclemp1  12865  setsslid  12927  imasival  13182  imasaddflemg  13192  grpinvalem  13261  issubmnd  13318  imasmnd  13329  isgrpinv  13430  grpinvssd  13453  pwssub  13489  imasgrp  13491  mulgnndir  13531  subginv  13561  subginvcl  13563  ghmpreima  13646  conjnsg  13661  srgidmlem  13784  ringidmlem  13828  imasring  13870  dvdsr01  13910  unitnegcl  13936  01eq0ring  13995  issubrng2  14016  subrginv  14043  subrgunit  14045  aprsym  14090  lmodvneg1  14136  lspsn  14222  isridlrng  14288  lidl0cl  14289  rspcl  14297  rspssid  14298  rnglidlmmgm  14302  2idlcpblrng  14329  quscrng  14339  rspsn  14340  znidom  14463  psrlinv  14490  psr1clfi  14494  topbas  14583  tgrest  14685  txss12  14782  mpomulcn  15082  cnplimclemle  15184  dvconstss  15214  efltlemlt  15290  coseq0q4123  15350  lgsval  15525  lgscllem  15528  gausslemma2dlem1a  15579  lgseisen  15595  lgsquadlem1  15598  lgsquadlem2  15599  2lgslem3a1  15618  2lgslem3b1  15619  2lgslem3c1  15620  2lgslem3d1  15621  2lgsoddprm  15634  neapmkvlem  16080