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  4514  mapen  6907  fival  7036  supelti  7068  supmaxti  7070  infminti  7093  xnegdi  9943  frecuzrdgsuc  10506  hashunlem  10896  2zsupmax  11391  xrmin1inf  11432  serf0  11517  fsumabs  11630  binomlem  11648  cvgratz  11697  efcllemp  11823  ef0lem  11825  tannegap  11893  modm1div  11965  divalglemnqt  12085  bitsfzolem  12118  lcmid  12248  hashdvds  12389  prmdivdiv  12405  odzcllem  12411  reumodprminv  12422  nnnn0modprm0  12424  pythagtrip  12452  pcmpt  12512  pockthg  12526  4sqlem9  12555  4sqleminfi  12566  4sqexercise1  12567  4sqlem11  12570  ennnfonelemkh  12629  ctinf  12647  nninfdclemcl  12665  nninfdclemp1  12667  setsslid  12729  imasival  12949  imasaddflemg  12959  grpinvalem  13028  issubmnd  13083  isgrpinv  13186  grpinvssd  13209  imasgrp  13241  mulgnndir  13281  subginv  13311  subginvcl  13313  ghmpreima  13396  conjnsg  13411  srgidmlem  13534  ringidmlem  13578  imasring  13620  dvdsr01  13660  unitnegcl  13686  01eq0ring  13745  issubrng2  13766  subrginv  13793  subrgunit  13795  aprsym  13840  lmodvneg1  13886  lspsn  13972  isridlrng  14038  lidl0cl  14039  rspcl  14047  rspssid  14048  rnglidlmmgm  14052  2idlcpblrng  14079  quscrng  14089  rspsn  14090  znidom  14213  topbas  14303  tgrest  14405  txss12  14502  mpomulcn  14802  cnplimclemle  14904  dvconstss  14934  efltlemlt  15010  coseq0q4123  15070  lgsval  15245  lgscllem  15248  gausslemma2dlem1a  15299  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgsoddprm  15354  neapmkvlem  15711