Theorem mp3an12i 1488

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  csbwrecsg  8301  oneo  8552  nnneo  8627  naddcllem  8648  ener  8984  sucdom2  9173  unxpdomlem3  9204  dfac2b  10089  ackbij2  10200  axgroth3  10791  mul02  11363  recreclt  12093  cju  12193  elnnnn0c  12528  elnnz1  12599  uz3m2nn  12897  iccen  13503  mptnn0fsupp  14012  hashgt23el  14439  hashfun  14452  hashf1lem1  14470  hash7g  14501  hash3tpexb  14509  funcnvs2  14928  remim  15146  iseraltlem2  15712  climcndslem1  15881  geo2lim  15907  fprodge0  16025  fprodge1  16027  absefib  16232  efieq1re  16233  3dvds  16367  oddp1d2  16394  bitsres  16509  phiprmpw  16813  pythagtriplem1  16854  symggen  19512  psgnuni  19541  lt6abl  19937  pws1  20375  0ringnnzr  20577  pmatcollpw2lem  22839  uzrest  23959  ressuss  24324  reperflem  24881  xrge0tsms  24897  cphsqrtcl  25248  ovolicopnf  25588  itg2seq  25806  itg2monolem2  25815  itgz  25845  ibl0  25851  iblss  25869  itgeqa  25878  iblconst  25882  iblabsr  25894  iblmulc2  25895  itgsplit  25900  tdeglem4  26122  dvnply2  26353  aannenlem2  26395  aannenlem3  26396  aalioulem2  26399  aaliou3lem2  26409  psercn  26491  abelth  26506  pilem3  26518  resinf1o  26603  efif1olem4  26612  logdivlti  26687  dvlog2lem  26719  efopn  26725  cxpsqrt  26770  isosctrlem1  26885  asinsin  26959  atanlogsub  26983  atanbnd  26993  atantayl2  27005  basellem2  27148  basellem3  27149  isnsqf  27201  ppidif  27229  1sgm2ppw  27266  ppiublem1  27268  bposlem6  27355  bposlem9  27358  gausslemma2dlem1  27432  lgseisenlem1  27441  lgseisen  27445  lgsquad3  27453  m1lgs  27454  ostth3  27704  cutbdaybnd  27890  cutbdaybnd2  27891  cutbdaylt  27893  madebdaylemlrcut  27994  bdayiun  28010  sltsbday  28012  cofcut1  28015  cofcutr  28019  negsproplem4  28126  negsproplem5  28127  negsproplem6  28128  precsexlem11  28312  pw2divscld  28534  pw2divmulsd  28535  pw2divscan2d  28537  pw2divsassd  28538  pw2divsrecd  28542  bdayfinbndlem1  28562  z12zsodd  28577  axlowdimlem3  29147  axlowdimlem7  29151  axlowdimlem16  29160  axlowdim  29164  umgr2v2e  29728  clwlkclwwlken  30216  clwwlken  30256  0wlkonlem2  30323  clwwlknonclwlknonen  30567  dlwwlknondlwlknonen  30570  eulerpartlemgvv  34675  lfuhgr2  35474  nmulprop  36545  poimirlem26  38150  mblfinlem2  38162  itg2addnclem3  38177  pr2cv  44129  isosctrlem1ALT  45514  fourierdlem48  46733  fourierdlem49  46734  fourierdlem113  46798  muldvdsfacgt  47985  fmtnorec1  48151  evengpoap3  48426  pgnioedg1  48735  pgnioedg2  48736  pgnioedg3  48737  pgnioedg4  48738  pgnioedg5  48739  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem5lem1  48747  pgnbgreunbgrlem5lem2  48748  pgnbgreunbgrlem5lem3  48749  line2x  49381  icccldii  49545