MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2an2r Structured version   Visualization version   GIF version

Theorem syl2an2r 893
Description: syl2anr 494 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)
Hypotheses
Ref Expression
syl2an2r.1 (𝜑𝜓)
syl2an2r.2 ((𝜑𝜒) → 𝜃)
syl2an2r.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2r ((𝜑𝜒) → 𝜏)

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.2 . 2 ((𝜑𝜒) → 𝜃)
2 syl2an2r.1 . . 3 (𝜑𝜓)
3 syl2an2r.3 . . 3 ((𝜓𝜃) → 𝜏)
42, 3sylan 487 . 2 ((𝜑𝜃) → 𝜏)
51, 4syldan 486 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff setvar class
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 197  df-an 385
This theorem is referenced by:  disjxiun  4681  brcogw  5323  ordtr3OLD  5808  funfni  6029  fvelimab  6292  dff3  6412  f1cofveqaeq  6555  grprinvlem  6914  boxcutc  7993  supmax  8414  cantnff  8609  infxpenlem  8874  cfsmolem  9130  tsken  9614  addmodlteq  12785  hashdifpr  13241  ccatalpha  13411  dvdsprmpweqle  15637  sylow1lem2  18060  lbsextlem2  19207  psrlinv  19445  mplsubglem  19482  mpllsslem  19483  evlslem1  19563  topbas  20824  clmvz  22957  gausslemma2dlem1a  25135  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2lgsoddprm  25186  uhgrspansubgrlem  26227  usgrres  26245  usgrnbcnvfv  26311  finsumvtxdg2sstep  26501  uspgr2wlkeq  26598  redwlk  26625  pthdivtx  26681  usgr2wlkspthlem2  26710  wwlknvtx  26793  2wlkdlem6  26896  umgr2wlkon  26915  rusgrnumwwlk  26942  clwwlknwwlksnb  27019  clwwnisshclwwsn  27024  clwwlknscsh  27027  1wlkdlem2  27116  fusgreghash2wsp  27318  2clwwlk2clwwlk  27338  numclwwlk6  27377  ofpreima2  29594  eulerpartlemgvv  30566  nosupbnd1lem4  31982  scutbdaylt  32047  gneispace  38749  ax6e2ndeqALT  39481  sineq0ALT  39487  setsv  41673  lighneal  41853  sprsymrelfolem2  42068
  Copyright terms: Public domain W3C validator