Theorem syl2an2r 597

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  4571  caofid0l  6254  caofid0r  6255  caofid1  6256  caofid2  6257  mapen  7020  fidcen  7074  fival  7153  supelti  7185  supmaxti  7187  infminti  7210  xnegdi  10081  frecuzrdgsuc  10653  hashunlem  11043  ccatrn  11162  ccatalpha  11166  swrdccat2  11224  pfxsuff1eqwrdeq  11252  ccatpfx  11254  swrdccatin2  11282  pfxccatin12lem2  11284  2zsupmax  11758  xrmin1inf  11799  serf0  11884  fsumabs  11997  binomlem  12015  cvgratz  12064  efcllemp  12190  ef0lem  12192  tannegap  12260  modm1div  12332  divalglemnqt  12452  bitsfzolem  12486  lcmid  12623  hashdvds  12764  prmdivdiv  12780  odzcllem  12786  reumodprminv  12797  nnnn0modprm0  12799  pythagtrip  12827  pcmpt  12887  pockthg  12901  4sqlem9  12930  4sqleminfi  12941  4sqexercise1  12942  4sqlem11  12945  ennnfonelemkh  13004  ctinf  13022  nninfdclemcl  13040  nninfdclemp1  13042  setsslid  13104  imasival  13360  imasaddflemg  13370  grpinvalem  13439  issubmnd  13496  imasmnd  13507  isgrpinv  13608  grpinvssd  13631  pwssub  13667  imasgrp  13669  mulgnndir  13709  subginv  13739  subginvcl  13741  ghmpreima  13824  conjnsg  13839  srgidmlem  13962  ringidmlem  14006  imasring  14048  dvdsr01  14089  unitnegcl  14115  01eq0ring  14174  issubrng2  14195  subrginv  14222  subrgunit  14224  aprsym  14269  lmodvneg1  14315  lspsn  14401  isridlrng  14467  lidl0cl  14468  rspcl  14476  rspssid  14477  rnglidlmmgm  14481  2idlcpblrng  14508  quscrng  14518  rspsn  14519  znidom  14642  psrlinv  14669  psr1clfi  14673  topbas  14762  tgrest  14864  txss12  14961  mpomulcn  15261  cnplimclemle  15363  dvconstss  15393  efltlemlt  15469  coseq0q4123  15529  lgsval  15704  lgscllem  15707  gausslemma2dlem1a  15758  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  2lgsoddprm  15813  uspgr2wlkeq  16137  neapmkvlem  16549