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

Theorem mp3an2i 1421
 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
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 1403 . 2 ((𝜒𝜃) → 𝜏)
61, 2, 5syl2anc 691 1 (𝜓𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ 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:  nnledivrp  11816  wrdlen2i  13534  0.999...  14451  fsumcube  14630  3dvds  14890  cnaddinv  18097  opsrtoslem2  19306  frgpcyg  19741  pt1hmeo  21419  cnheiborlem  22561  lgsqrlem4  24874  gausslemma2dlem4  24894  lgsquad2lem2  24910  enrelmap  37311  k0004lem3  37467  sineq0ALT  38195  odz2prm2pw  40013  fmtno4prmfac  40022  lighneallem3  40062  lighneallem4a  40063  lighneallem4  40065  1wlkp1lem3  40884  1wlkp1lem7  40888  1wlkp1lem8  40889  pthdlem1  40972  conngrv2edg  41362
 Copyright terms: Public domain W3C validator