Theorem mp3an12i 1467

Description: mp3an 1463 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

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1453	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  csbwrecsg  8251  oneo  8499  nnneo  8573  naddcllem  8594  ener  8926  sucdom2  9117  unxpdomlem3  9147  dfac2b  10025  ackbij2  10136  axgroth3  10725  mul02  11294  recreclt  12024  cju  12124  elnnnn0c  12429  elnnz1  12501  eluzsubiOLD  12769  uz3m2nn  12795  iccen  13400  mptnn0fsupp  13904  hashgt23el  14331  hashfun  14344  hashf1lem1  14362  hash7g  14393  hash3tpexb  14401  funcnvs2  14820  remim  15024  iseraltlem2  15590  climcndslem1  15756  geo2lim  15782  fprodge0  15900  fprodge1  15902  absefib  16107  efieq1re  16108  3dvds  16242  oddp1d2  16269  bitsres  16384  phiprmpw  16687  pythagtriplem1  16728  symggen  19349  psgnuni  19378  lt6abl  19774  pws1  20210  0ringnnzr  20410  pmatcollpw2lem  22662  uzrest  23782  ressuss  24148  reperflem  24705  xrge0tsms  24721  cphsqrtcl  25082  ovolicopnf  25423  itg2seq  25641  itg2monolem2  25650  itgz  25680  ibl0  25686  iblss  25704  itgeqa  25713  iblconst  25717  iblabsr  25729  iblmulc2  25730  itgsplit  25735  tdeglem4  25963  dvnply2  26193  aannenlem2  26235  aannenlem3  26236  aalioulem2  26239  aaliou3lem2  26249  psercn  26334  abelth  26349  pilem3  26361  resinf1o  26443  efif1olem4  26452  logdivlti  26527  dvlog2lem  26559  efopn  26565  cxpsqrt  26610  isosctrlem1  26726  asinsin  26800  atanlogsub  26824  atanbnd  26834  atantayl2  26846  basellem2  26990  basellem3  26991  isnsqf  27043  ppidif  27071  1sgm2ppw  27109  ppiublem1  27111  bposlem6  27198  bposlem9  27201  gausslemma2dlem1  27275  lgseisenlem1  27284  lgseisen  27288  lgsquad3  27296  m1lgs  27297  ostth3  27547  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  madebdaylemlrcut  27815  bdayiun  27831  cofcut1  27835  cofcutr  27839  negsproplem4  27944  negsproplem5  27945  negsproplem6  27946  precsexlem11  28126  pw2divscld  28333  pw2divsmuld  28334  pw2divscan2d  28336  pw2divsassd  28337  pw2divsrecd  28341  zs12zodd  28363  axlowdimlem3  28893  axlowdimlem7  28897  axlowdimlem16  28906  axlowdim  28910  umgr2v2e  29475  clwlkclwwlken  29960  clwwlken  30000  0wlkonlem2  30067  clwwlknonclwlknonen  30311  dlwwlknondlwlknonen  30314  eulerpartlemgvv  34360  lfuhgr2  35112  poimirlem26  37646  mblfinlem2  37658  itg2addnclem3  37673  pr2cv  43541  isosctrlem1ALT  44927  fmtnorec1  47541  evengpoap3  47803  pgnioedg1  48112  pgnioedg2  48113  pgnioedg3  48114  pgnioedg4  48115  pgnioedg5  48116  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem5lem1  48124  pgnbgreunbgrlem5lem2  48125  pgnbgreunbgrlem5lem3  48126  line2x  48759  icccldii  48923