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

Theorem mp3an12i 1420
Description: mp3an 1416 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
Hypotheses
Ref Expression
mp3an12i.1 𝜑
mp3an12i.2 𝜓
mp3an12i.3 (𝜒𝜃)
mp3an12i.4 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
mp3an12i (𝜒𝜏)

Proof of Theorem mp3an12i
StepHypRef Expression
1 mp3an12i.3 . 2 (𝜒𝜃)
2 mp3an12i.1 . . 3 𝜑
3 mp3an12i.2 . . 3 𝜓
4 mp3an12i.4 . . 3 ((𝜑𝜓𝜃) → 𝜏)
52, 3, 4mp3an12 1406 . 2 (𝜃𝜏)
61, 5syl 17 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:  ener  7888  hashfun  13084  funcnvs2  13508  3dvds  14890  oddp1d2  14920  bitsres  15033  bposlem9  24817  gausslemma2dlem1  24891  poimirlem26  32605  mblfinlem2  32617  isosctrlem1ALT  38192  fmtnorec1  39987  evengpoap3  40215  umgr2v2e  40741  0wlkOnlem2  41287
  Copyright terms: Public domain W3C validator