Theorem syl2an2r 585

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 568	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  4408  mapen  6748  fival  6866  supelti  6897  supmaxti  6899  infminti  6922  xnegdi  9681  frecuzrdgsuc  10218  hashunlem  10582  2zsupmax  11029  xrmin1inf  11068  serf0  11153  fsumabs  11266  binomlem  11284  cvgratz  11333  efcllemp  11401  ef0lem  11403  tannegap  11471  divalglemnqt  11653  lcmid  11797  hashdvds  11933  ennnfonelemkh  11961  ctinf  11979  setsslid  12048  topbas  12275  tgrest  12377  txss12  12474  cnplimclemle  12845  efltlemlt  12903  coseq0q4123  12963  neapmkvlem  13424