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

Theorem mp3an3an 1469
Description: mp3an 1463 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 1450 . 2 ((𝜒𝜏) → 𝜂)
61, 2, 5syl2an 596 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  mp3an2ani  1470  unfilem2  9344  rankelun  9912  mul02  11439  fnn0ind  12717  supminf  12977  nn0p1elfzo  13742  faclbnd5  14337  pfxccatin12lem3  14770  mulre  15160  divalglem0  16430  algcvga  16616  infpn2  16951  prmgaplem7  17095  blssioo  24816  i1fsub  25743  itg1sub  25744  coesub  26296  dgrsub  26312  sincosq1eq  26554  logtayl2  26704  cxploglim  27021  uspgr2v1e2w  29268  ftc1anclem6  37705  plusmod5ne  47347  io1ii  48818
  Copyright terms: Public domain W3C validator