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

Theorem mp3an12i 1465
Description: mp3an 1461 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 1451 . 2 (𝜃𝜏)
61, 5syl 17 1 (𝜒𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 398  df-3an 1089
This theorem is referenced by:  csbwrecsg  8168  oneo  8443  nnneo  8516  ener  8822  sucdom2  9027  unxpdomlem3  9073  dfac2b  9936  ackbij2  10049  axgroth3  10637  mul02  11203  recreclt  11924  cju  12019  elnnnn0c  12328  elnnz1  12396  eluzsubi  12662  uz3m2nn  12681  iccen  13279  mptnn0fsupp  13767  hashgt23el  14188  hashfun  14201  hashf1lem1  14217  hashf1lem1OLD  14218  funcnvs2  14675  remim  14877  iseraltlem2  15443  climcndslem1  15610  geo2lim  15636  fprodge0  15752  fprodge1  15754  absefib  15956  efieq1re  15957  3dvds  16089  oddp1d2  16116  bitsres  16229  phiprmpw  16526  pythagtriplem1  16566  symggen  19127  psgnuni  19156  lt6abl  19545  pws1  19904  0ringnnzr  20589  pmatcollpw2lem  21975  uzrest  23097  ressuss  23463  reperflem  24030  xrge0tsms  24046  cphsqrtcl  24397  ovolicopnf  24737  itg2seq  24956  itg2monolem2  24965  itgz  24994  ibl0  25000  iblss  25018  itgeqa  25027  iblconst  25031  iblabsr  25043  iblmulc2  25044  itgsplit  25049  tdeglem4  25273  tdeglem4OLD  25274  dvnply2  25496  aannenlem2  25538  aannenlem3  25539  aalioulem2  25542  aaliou3lem2  25552  psercn  25634  abelth  25649  pilem3  25661  resinf1o  25741  efif1olem4  25750  logdivlti  25824  dvlog2lem  25856  efopn  25862  cxpsqrt  25907  isosctrlem1  26017  asinsin  26091  atanlogsub  26115  atanbnd  26125  atantayl2  26137  basellem2  26280  basellem3  26281  isnsqf  26333  ppidif  26361  1sgm2ppw  26397  ppiublem1  26399  bposlem6  26486  bposlem9  26489  gausslemma2dlem1  26563  lgseisenlem1  26572  lgseisen  26576  lgsquad3  26584  m1lgs  26585  ostth3  26835  axlowdimlem3  27361  axlowdimlem7  27365  axlowdimlem16  27374  axlowdim  27378  umgr2v2e  27941  clwlkclwwlken  28425  clwwlken  28465  0wlkonlem2  28532  clwwlknonclwlknonen  28776  dlwwlknondlwlknonen  28779  eulerpartlemgvv  32392  lfuhgr2  33129  naddcllem  33880  scutbdaybnd  34058  scutbdaybnd2  34059  scutbdaylt  34061  madebdaylemlrcut  34128  cofcut1  34139  cofcutr  34141  poimirlem26  35851  mblfinlem2  35863  itg2addnclem3  35878  pr2cv  41368  isosctrlem1ALT  42767  fmtnorec1  45233  evengpoap3  45495  line2x  46344  icccldii  46456
  Copyright terms: Public domain W3C validator