Theorem mp3an12i 1455

Description: mp3an 1451 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 1441	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  oneo  8048  nnneo  8119  ener  8394  unxpdomlem3  8560  dfac2b  9391  ackbij2  9500  axgroth3  10088  mul02  10654  recreclt  11376  cju  11471  elnnnn0c  11779  elnnz1  11846  eluzsubi  12110  uz3m2nn  12129  iccen  12722  mptnn0fsupp  13203  hashgt23el  13621  hashfun  13634  hashf1lem1  13649  funcnvs2  14099  remim  14298  iseraltlem2  14861  climcndslem1  15025  geo2lim  15052  fprodge0  15168  fprodge1  15170  absefib  15372  efieq1re  15373  3dvds  15501  oddp1d2  15528  bitsres  15643  phiprmpw  15930  pythagtriplem1  15970  symggen  18317  psgnuni  18346  lt6abl  18724  pws1  19044  0ringnnzr  19719  pmatcollpw2lem  21057  uzrest  22177  ressuss  22543  reperflem  23097  xrge0tsms  23113  cphsqrtcl  23459  ovolicopnf  23796  itg2seq  24014  itg2monolem2  24023  itgz  24052  ibl0  24058  iblss  24076  itgeqa  24085  iblconst  24089  iblabsr  24101  iblmulc2  24102  itgsplit  24107  tdeglem4  24325  dvnply2  24547  aannenlem2  24589  aannenlem3  24590  aalioulem2  24593  aaliou3lem2  24603  psercn  24685  abelth  24700  pilem3  24712  resinf1o  24789  efif1olem4  24798  logdivlti  24872  dvlog2lem  24904  efopn  24910  cxpsqrt  24955  isosctrlem1  25065  asinsin  25139  atanlogsub  25163  atanbnd  25173  atantayl2  25185  basellem2  25329  basellem3  25330  isnsqf  25382  ppidif  25410  1sgm2ppw  25446  ppiublem1  25448  bposlem6  25535  bposlem9  25538  gausslemma2dlem1  25612  lgseisenlem1  25621  lgseisen  25625  lgsquad3  25633  m1lgs  25634  ostth3  25884  axlowdimlem3  26401  axlowdimlem7  26405  axlowdimlem16  26414  axlowdim  26418  umgr2v2e  26978  clwlkclwwlken  27465  clwwlken  27506  0wlkonlem2  27573  clwwlknonclwlknonen  27822  dlwwlknondlwlknonen  27825  eulerpartlemgvv  31207  lfuhgr2  31933  scutbdaybnd  32829  scutbdaylt  32830  poimirlem26  34395  mblfinlem2  34407  pr2cv  39343  isosctrlem1ALT  40759  fmtnorec1  43135  evengpoap3  43400  line2x  44176