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  4464  mapen  6824  fival  6947  supelti  6979  supmaxti  6981  infminti  7004  xnegdi  9825  frecuzrdgsuc  10370  hashunlem  10739  2zsupmax  11189  xrmin1inf  11230  serf0  11315  fsumabs  11428  binomlem  11446  cvgratz  11495  efcllemp  11621  ef0lem  11623  tannegap  11691  modm1div  11762  divalglemnqt  11879  lcmid  12034  hashdvds  12175  prmdivdiv  12191  odzcllem  12196  reumodprminv  12207  nnnn0modprm0  12209  pythagtrip  12237  pcmpt  12295  pockthg  12309  4sqlem9  12338  ennnfonelemkh  12367  ctinf  12385  nninfdclemp1  12405  setsslid  12466  grprinvlem  12639  isgrpinv  12756  topbas  12861  tgrest  12963  txss12  13060  cnplimclemle  13431  efltlemlt  13489  coseq0q4123  13549  lgsval  13699  lgscllem  13702  neapmkvlem  14098