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

Theorem mp3an3an 1422
 Description: mp3an 1416 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 1403 . 2 ((𝜒𝜏) → 𝜂)
61, 2, 5syl2an 493 1 ((𝜓𝜃) → 𝜂)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  mp3an2ani  1423  nn0p1elfzo  12378
 Copyright terms: Public domain W3C validator