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

Theorem mp3an12i 1462
Description: mp3an 1458 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 1448 . 2 (𝜃𝜏)
61, 5syl 17 1 (𝜒𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  oneo  8194  nnneo  8265  ener  8543  unxpdomlem3  8712  dfac2b  9545  ackbij2  9658  axgroth3  10246  mul02  10811  recreclt  11532  cju  11625  elnnnn0c  11934  elnnz1  12000  eluzsubi  12264  uz3m2nn  12283  iccen  12879  mptnn0fsupp  13364  hashgt23el  13785  hashfun  13798  hashf1lem1  13813  funcnvs2  14270  remim  14471  iseraltlem2  15034  climcndslem1  15199  geo2lim  15226  fprodge0  15342  fprodge1  15344  absefib  15546  efieq1re  15547  3dvds  15675  oddp1d2  15702  bitsres  15815  phiprmpw  16106  pythagtriplem1  16146  symggen  18593  psgnuni  18622  lt6abl  19011  pws1  19365  0ringnnzr  20038  pmatcollpw2lem  21385  uzrest  22505  ressuss  22872  reperflem  23426  xrge0tsms  23442  cphsqrtcl  23792  ovolicopnf  24131  itg2seq  24349  itg2monolem2  24358  itgz  24387  ibl0  24393  iblss  24411  itgeqa  24420  iblconst  24424  iblabsr  24436  iblmulc2  24437  itgsplit  24442  tdeglem4  24664  dvnply2  24886  aannenlem2  24928  aannenlem3  24929  aalioulem2  24932  aaliou3lem2  24942  psercn  25024  abelth  25039  pilem3  25051  resinf1o  25131  efif1olem4  25140  logdivlti  25214  dvlog2lem  25246  efopn  25252  cxpsqrt  25297  isosctrlem1  25407  asinsin  25481  atanlogsub  25505  atanbnd  25515  atantayl2  25527  basellem2  25670  basellem3  25671  isnsqf  25723  ppidif  25751  1sgm2ppw  25787  ppiublem1  25789  bposlem6  25876  bposlem9  25879  gausslemma2dlem1  25953  lgseisenlem1  25962  lgseisen  25966  lgsquad3  25974  m1lgs  25975  ostth3  26225  axlowdimlem3  26741  axlowdimlem7  26745  axlowdimlem16  26754  axlowdim  26758  umgr2v2e  27318  clwlkclwwlken  27800  clwwlken  27840  0wlkonlem2  27907  clwwlknonclwlknonen  28151  dlwwlknondlwlknonen  28154  eulerpartlemgvv  31742  lfuhgr2  32473  scutbdaybnd  33383  scutbdaylt  33384  poimirlem26  35076  mblfinlem2  35088  itg2addnclem3  35103  pr2cv  40234  isosctrlem1ALT  41627  fmtnorec1  44041  evengpoap3  44304  line2x  45155
  Copyright terms: Public domain W3C validator