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 1089

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 1091

This theorem is referenced by:  oneo  8287  nnneo  8358  ener  8653  unxpdomlem3  8860  dfac2b  9709  ackbij2  9822  axgroth3  10410  mul02  10975  recreclt  11696  cju  11791  elnnnn0c  12100  elnnz1  12168  eluzsubi  12433  uz3m2nn  12452  iccen  13050  mptnn0fsupp  13535  hashgt23el  13956  hashfun  13969  hashf1lem1  13985  hashf1lem1OLD  13986  funcnvs2  14443  remim  14645  iseraltlem2  15211  climcndslem1  15376  geo2lim  15402  fprodge0  15518  fprodge1  15520  absefib  15722  efieq1re  15723  3dvds  15855  oddp1d2  15882  bitsres  15995  phiprmpw  16292  pythagtriplem1  16332  symggen  18816  psgnuni  18845  lt6abl  19234  pws1  19588  0ringnnzr  20261  pmatcollpw2lem  21628  uzrest  22748  ressuss  23114  reperflem  23669  xrge0tsms  23685  cphsqrtcl  24035  ovolicopnf  24375  itg2seq  24594  itg2monolem2  24603  itgz  24632  ibl0  24638  iblss  24656  itgeqa  24665  iblconst  24669  iblabsr  24681  iblmulc2  24682  itgsplit  24687  tdeglem4  24911  tdeglem4OLD  24912  dvnply2  25134  aannenlem2  25176  aannenlem3  25177  aalioulem2  25180  aaliou3lem2  25190  psercn  25272  abelth  25287  pilem3  25299  resinf1o  25379  efif1olem4  25388  logdivlti  25462  dvlog2lem  25494  efopn  25500  cxpsqrt  25545  isosctrlem1  25655  asinsin  25729  atanlogsub  25753  atanbnd  25763  atantayl2  25775  basellem2  25918  basellem3  25919  isnsqf  25971  ppidif  25999  1sgm2ppw  26035  ppiublem1  26037  bposlem6  26124  bposlem9  26127  gausslemma2dlem1  26201  lgseisenlem1  26210  lgseisen  26214  lgsquad3  26222  m1lgs  26223  ostth3  26473  axlowdimlem3  26989  axlowdimlem7  26993  axlowdimlem16  27002  axlowdim  27006  umgr2v2e  27567  clwlkclwwlken  28049  clwwlken  28089  0wlkonlem2  28156  clwwlknonclwlknonen  28400  dlwwlknondlwlknonen  28403  eulerpartlemgvv  32009  lfuhgr2  32747  naddcllem  33517  scutbdaybnd  33695  scutbdaybnd2  33696  scutbdaylt  33698  madebdaylemlrcut  33765  cofcut1  33776  cofcutr  33778  poimirlem26  35489  mblfinlem2  35501  itg2addnclem3  35516  pr2cv  40772  isosctrlem1ALT  42168  fmtnorec1  44605  evengpoap3  44867  line2x  45716  icccldii  45828