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  4494  mapen  6864  fival  6987  supelti  7019  supmaxti  7021  infminti  7044  xnegdi  9886  frecuzrdgsuc  10432  hashunlem  10802  2zsupmax  11252  xrmin1inf  11293  serf0  11378  fsumabs  11491  binomlem  11509  cvgratz  11558  efcllemp  11684  ef0lem  11686  tannegap  11754  modm1div  11825  divalglemnqt  11943  lcmid  12098  hashdvds  12239  prmdivdiv  12255  odzcllem  12260  reumodprminv  12271  nnnn0modprm0  12273  pythagtrip  12301  pcmpt  12359  pockthg  12373  4sqlem9  12402  ennnfonelemkh  12431  ctinf  12449  nninfdclemcl  12467  nninfdclemp1  12469  setsslid  12531  imasival  12749  imasaddflemg  12759  grpinvalem  12827  issubmnd  12869  isgrpinv  12964  grpinvssd  12987  imasgrp  13019  mulgnndir  13057  subginv  13086  subginvcl  13088  ghmpreima  13166  conjnsg  13181  srgidmlem  13293  ringidmlem  13337  imasring  13375  dvdsr01  13415  unitnegcl  13441  01eq0ring  13497  issubrng2  13518  subrginv  13545  subrgunit  13547  aprsym  13561  lmodvneg1  13607  lspsn  13693  isridlrng  13759  lidl0cl  13760  rspcl  13768  rspssid  13769  rnglidlmmgm  13773  2idlcpblrng  13799  quscrng  13808  topbas  13964  tgrest  14066  txss12  14163  cnplimclemle  14534  efltlemlt  14592  coseq0q4123  14652  lgsval  14802  lgscllem  14805  neapmkvlem  15213