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

Theorem mp3an3an 1458
Description: mp3an 1452 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an3an.1 𝜑
mp3an3an.2 (𝜓𝜒)
mp3an3an.3 (𝜃𝜏)
mp3an3an.4 ((𝜑𝜒𝜏) → 𝜂)
Assertion
Ref Expression
mp3an3an ((𝜓𝜃) → 𝜂)

Proof of Theorem mp3an3an
StepHypRef Expression
1 mp3an3an.2 . 2 (𝜓𝜒)
2 mp3an3an.3 . 2 (𝜃𝜏)
3 mp3an3an.1 . . 3 𝜑
4 mp3an3an.4 . . 3 ((𝜑𝜒𝜏) → 𝜂)
53, 4mp3an1 1439 . 2 ((𝜒𝜏) → 𝜂)
61, 2, 5syl2an 595 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  mp3an2ani  1459  unfilem2  8771  rankelun  9289  mul02  10806  fnn0ind  12069  supminf  12323  nn0p1elfzo  13068  faclbnd5  13646  pfxccatin12lem3  14082  mulre  14468  divalglem0  15732  algcvga  15911  infpn2  16237  prmgaplem7  16381  blssioo  23330  i1fsub  24236  itg1sub  24237  coesub  24774  dgrsub  24789  sincosq1eq  25025  logtayl2  25172  cxploglim  25482  uspgr2v1e2w  26960  ftc1anclem6  34853
  Copyright terms: Public domain W3C validator