Theorem mp3an12i 1493

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  csbwrecsg  8313  oneo  8564  nnneo  8639  naddcllem  8660  ener  8996  sucdom2  9185  unxpdomlem3  9216  dfac2b  10121  ackbij2  10232  axgroth3  10822  mul02  11394  recreclt  12120  cju  12220  elnnnn0c  12555  elnnz1  12626  uz3m2nn  12924  iccen  13530  mptnn0fsupp  14040  hashgt23el  14468  hashfun  14481  hashf1lem1  14499  hash7g  14530  hash3tpexb  14538  funcnvs2  14957  remim  15175  iseraltlem2  15741  climcndslem1  15910  geo2lim  15936  fprodge0  16054  fprodge1  16056  absefib  16260  efieq1re  16261  3dvds  16395  oddp1d2  16422  bitsres  16537  phiprmpw  16841  pythagtriplem1  16882  symggen  19546  psgnuni  19575  lt6abl  19971  pws1  20413  0ringnnzr  20634  pmatcollpw2lem  22945  uzrest  24065  ressuss  24430  reperflem  24987  xrge0tsms  25003  cphsqrtcl  25354  ovolicopnf  25694  itg2seq  25912  itg2monolem2  25921  itgz  25951  ibl0  25957  iblss  25975  itgeqa  25984  iblconst  25988  iblabsr  26000  iblmulc2  26001  itgsplit  26006  tdeglem4  26228  dvnply2  26459  aannenlem2  26503  aannenlem3  26504  aalioulem2  26507  aaliou3lem2  26517  psercn  26600  abelth  26615  pilem3  26627  resinf1o  26712  efif1olem4  26721  logdivlti  26796  dvlog2lem  26828  efopn  26834  cxpsqrt  26879  isosctrlem1  26994  asinsin  27068  atanlogsub  27092  atanbnd  27102  atantayl2  27114  basellem2  27257  basellem3  27258  isnsqf  27310  ppidif  27338  1sgm2ppw  27375  ppiublem1  27377  bposlem6  27464  bposlem9  27467  gausslemma2dlem1  27541  lgseisenlem1  27550  lgseisen  27554  lgsquad3  27562  m1lgs  27563  ostth3  27813  cutbdaybnd  27999  cutbdaybnd2  28000  cutbdaylt  28002  madebdaylemlrcut  28103  bdayiun  28119  sltsbday  28121  cofcut1  28124  cofcutr  28128  negsproplem4  28235  negsproplem5  28236  negsproplem6  28237  precsexlem11  28421  pw2divscld  28643  pw2divmulsd  28644  pw2divscan2d  28646  pw2divsassd  28647  pw2divsrecd  28651  bdayfinbndlem1  28671  z12zsodd  28686  axlowdimlem3  29305  axlowdimlem7  29309  axlowdimlem16  29318  axlowdim  29322  umgr2v2e  29886  clwlkclwwlken  30374  clwwlken  30414  0wlkonlem2  30481  clwwlknonclwlknonen  30725  dlwwlknondlwlknonen  30728  eulerpartlemgvv  34775  lfuhgr2  35619  nmulprop  36690  poimirlem26  38325  mblfinlem2  38337  itg2addnclem3  38352  pr2cv  44302  isosctrlem1ALT  45670  fourierdlem48  46896  fourierdlem49  46897  fourierdlem113  46961  muldvdsfacgt  48151  fmtnorec1  48317  evengpoap3  48592  pgnioedg1  48901  pgnioedg2  48902  pgnioedg3  48903  pgnioedg4  48904  pgnioedg5  48905  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem5lem1  48913  pgnbgreunbgrlem5lem2  48914  pgnbgreunbgrlem5lem3  48915  line2x  49562  icccldii  49725