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

Theorem mp3an12i 1576
Description: mp3an 1572 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 1562 . 2 (𝜃𝜏)
61, 5syl 17 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:  ener  8160  dfac2b  9157  hashfun  13426  funcnvs2  13867  3dvds  15261  oddp1d2  15290  bitsres  15403  pilem3  24427  bposlem9  25238  gausslemma2dlem1  25312  umgr2v2e  26656  clwlkclwwlken  27162  clwwlken  27208  0wlkonlem2  27299  clwwlknonclwlknonen  27552  dlwwlknondlwlknonen  27557  eulerpartlemgvv  30778  scutbdaybnd  32258  scutbdaylt  32259  poimirlem26  33768  mblfinlem2  33780  isosctrlem1ALT  39692  fmtnorec1  41974  evengpoap3  42212
  Copyright terms: Public domain W3C validator