Theorem syl2an2r 872

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

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  disjxiun  4579  brcogw  5212  ordtr3OLD  5687  funfni  5905  fvelimab  6163  dff3  6280  cantnff  8454  infxpenlem  8719  cfsmolem  8975  addmodlteq  12607  hashdifpr  13064  ccatalpha  13228  dvdsprmpweqle  15428  sylow1lem2  17837  lbsextlem2  18980  psrlinv  19218  mplsubglem  19255  mpllsslem  19256  evlslem1  19336  clmvz  22719  gausslemma2dlem1a  24890  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  2lgsoddprm  24941  ofpreima2  28849  gneispace  37452  ax6e2ndeqALT  38189  sineq0ALT  38195  lighneal  40066  f1cofveqaeq  40323  uspgr2wlkeq  40854  red1wlk  40881  pthdivtx  40935  usgr2wlkspthlem2  40964  21wlkdlem6  41138  umgr2wlkon  41157  rusgrnumwwlk  41178  clwwlksnscsh  41247  11wlkdlem2  41305  fusgreghash2wsp  41502  av-numclwwlkovf2ex  41517  av-numclwwlk6  41544