Theorem syl2an2r 590

Description: syl2anr 288 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 287	. 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜒)) → 𝜏)
5	4	anabss5 573	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  op1stbg  4462  mapen  6822  fival  6945  supelti  6977  supmaxti  6979  infminti  7002  xnegdi  9818  frecuzrdgsuc  10363  hashunlem  10732  2zsupmax  11182  xrmin1inf  11223  serf0  11308  fsumabs  11421  binomlem  11439  cvgratz  11488  efcllemp  11614  ef0lem  11616  tannegap  11684  modm1div  11755  divalglemnqt  11872  lcmid  12027  hashdvds  12168  prmdivdiv  12184  odzcllem  12189  reumodprminv  12200  nnnn0modprm0  12202  pythagtrip  12230  pcmpt  12288  pockthg  12302  4sqlem9  12331  ennnfonelemkh  12360  ctinf  12378  nninfdclemp1  12398  setsslid  12459  grprinvlem  12632  topbas  12826  tgrest  12928  txss12  13025  cnplimclemle  13396  efltlemlt  13454  coseq0q4123  13514  lgsval  13664  lgscllem  13667  neapmkvlem  14063