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

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

Proof of Theorem mp3an2i
StepHypRef Expression
1 mp3an2i.2 . 2 (𝜓𝜒)
2 mp3an2i.3 . 2 (𝜓𝜃)
3 mp3an2i.1 . . 3 𝜑
4 mp3an2i.4 . . 3 ((𝜑𝜒𝜃) → 𝜏)
53, 4mp3an1 1408 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 692 1 (𝜓𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  nnledivrp  11900  wrdlen2i  13636  0.999...  14556  fsumcube  14735  3dvds  14995  cnaddinv  18214  opsrtoslem2  19425  frgpcyg  19862  pt1hmeo  21549  cnheiborlem  22693  lgsqrlem4  25008  gausslemma2dlem4  25028  lgsquad2lem2  25044  wlkp1lem3  26475  wlkp1lem7  26479  wlkp1lem8  26480  pthdlem1  26565  conngrv2edg  26955  enrelmap  37812  k0004lem3  37968  sineq0ALT  38695  odz2prm2pw  40804  fmtno4prmfac  40813  lighneallem3  40853  lighneallem4a  40854  lighneallem4  40856
  Copyright terms: Public domain W3C validator