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

Theorem mp3an2i 1577
Description: mp3an 1572 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 1559 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 573 1 (𝜓𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  nnledivrp  12145  wrdlen2i  13896  sqrlem7  14197  0.999...  14819  fsumcube  14997  3dvds  15261  nno  15306  divgcdodd  15629  cnaddinv  18481  opsrtoslem2  19700  frgpcyg  20137  pt1hmeo  21830  cnheiborlem  22973  lgsqrlem4  25295  gausslemma2dlem4  25315  lgsquad2lem2  25331  wlkp1lem3  26807  wlkp1lem7  26811  wlkp1lem8  26812  pthdlem1  26897  conngrv2edg  27375  cvmlift2lem10  31632  frrlem11  32129  nosupbday  32188  enrelmap  38817  k0004lem3  38973  sineq0ALT  39695  xlimconst  40566  odz2prm2pw  42000  fmtno4prmfac  42009  lighneallem3  42049  lighneallem4a  42050  lighneallem4  42052
  Copyright terms: Public domain W3C validator