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  4477  mapen  6841  fival  6964  supelti  6996  supmaxti  6998  infminti  7021  xnegdi  9862  frecuzrdgsuc  10407  hashunlem  10775  2zsupmax  11225  xrmin1inf  11266  serf0  11351  fsumabs  11464  binomlem  11482  cvgratz  11531  efcllemp  11657  ef0lem  11659  tannegap  11727  modm1div  11798  divalglemnqt  11915  lcmid  12070  hashdvds  12211  prmdivdiv  12227  odzcllem  12232  reumodprminv  12243  nnnn0modprm0  12245  pythagtrip  12273  pcmpt  12331  pockthg  12345  4sqlem9  12374  ennnfonelemkh  12403  ctinf  12421  nninfdclemp1  12441  setsslid  12503  grprinvlem  12734  issubmnd  12773  isgrpinv  12854  grpinvssd  12875  mulgnndir  12939  subginv  12967  subginvcl  12969  srgidmlem  13061  ringidmlem  13105  dvdsr01  13172  unitnegcl  13198  01eq0ring  13229  aprsym  13241  topbas  13349  tgrest  13451  txss12  13548  cnplimclemle  13919  efltlemlt  13977  coseq0q4123  14037  lgsval  14187  lgscllem  14190  neapmkvlem  14585