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

Theorem mp3an2i 1591
Description: mp3an 1586 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 1573 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 580 1 (𝜓𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  nnledivrp  12183  wrdlen2i  14024  sqrlem7  14327  0.999...  14947  fsumcube  15124  sin01gt0  15253  cos01gt0  15254  3dvds  15388  nno  15431  divgcdodd  15752  cnaddinv  18586  opsrtoslem2  19804  frgpcyg  20240  pt1hmeo  21935  metustid  22684  cnheiborlem  23078  lgsqrlem4  25423  gausslemma2dlem4  25443  lgsquad2lem2  25459  wlkp1lem3  26920  wlkp1lem7  26924  wlkp1lem8  26925  pthdlem1  27012  conngrv2edg  27531  cvmlift2lem10  31803  frrlem11  32297  nosupbday  32356  itg2gt0cn  33945  enrelmap  39061  k0004lem3  39217  sineq0ALT  39921  xlimconst  40783  odz2prm2pw  42245  fmtno4prmfac  42254  lighneallem3  42294  lighneallem4a  42295  lighneallem4  42297
  Copyright terms: Public domain W3C validator