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

Theorem mp3an3an 1464
Description: mp3an 1458 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 1445 . 2 ((𝜒𝜏) → 𝜂)
61, 2, 5syl2an 598 1 ((𝜓𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  mp3an2ani  1465  unfilem2  8771  rankelun  9289  mul02  10807  fnn0ind  12069  supminf  12323  nn0p1elfzo  13075  faclbnd5  13654  pfxccatin12lem3  14085  mulre  14471  divalglem0  15733  algcvga  15912  infpn2  16238  prmgaplem7  16382  blssioo  23398  i1fsub  24310  itg1sub  24311  coesub  24852  dgrsub  24867  sincosq1eq  25103  logtayl2  25251  cxploglim  25561  uspgr2v1e2w  27039  ftc1anclem6  35097
  Copyright terms: Public domain W3C validator