Theorem mp3an12i 1466

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  csbwrecsg  8306  oneo  8581  nnneo  8654  naddcllem  8675  ener  8997  sucdom2  9206  unxpdomlem3  9252  dfac2b  10125  ackbij2  10238  axgroth3  10826  mul02  11392  recreclt  12113  cju  12208  elnnnn0c  12517  elnnz1  12588  eluzsubiOLD  12856  uz3m2nn  12875  iccen  13474  mptnn0fsupp  13962  hashgt23el  14384  hashfun  14397  hashf1lem1  14415  hashf1lem1OLD  14416  funcnvs2  14864  remim  15064  iseraltlem2  15629  climcndslem1  15795  geo2lim  15821  fprodge0  15937  fprodge1  15939  absefib  16141  efieq1re  16142  3dvds  16274  oddp1d2  16301  bitsres  16414  phiprmpw  16709  pythagtriplem1  16749  symggen  19338  psgnuni  19367  lt6abl  19763  pws1  20138  0ringnnzr  20302  pmatcollpw2lem  22279  uzrest  23401  ressuss  23767  reperflem  24334  xrge0tsms  24350  cphsqrtcl  24701  ovolicopnf  25041  itg2seq  25260  itg2monolem2  25269  itgz  25298  ibl0  25304  iblss  25322  itgeqa  25331  iblconst  25335  iblabsr  25347  iblmulc2  25348  itgsplit  25353  tdeglem4  25577  tdeglem4OLD  25578  dvnply2  25800  aannenlem2  25842  aannenlem3  25843  aalioulem2  25846  aaliou3lem2  25856  psercn  25938  abelth  25953  pilem3  25965  resinf1o  26045  efif1olem4  26054  logdivlti  26128  dvlog2lem  26160  efopn  26166  cxpsqrt  26211  isosctrlem1  26323  asinsin  26397  atanlogsub  26421  atanbnd  26431  atantayl2  26443  basellem2  26586  basellem3  26587  isnsqf  26639  ppidif  26667  1sgm2ppw  26703  ppiublem1  26705  bposlem6  26792  bposlem9  26795  gausslemma2dlem1  26869  lgseisenlem1  26878  lgseisen  26882  lgsquad3  26890  m1lgs  26891  ostth3  27141  scutbdaybnd  27316  scutbdaybnd2  27317  scutbdaylt  27319  madebdaylemlrcut  27393  cofcut1  27407  cofcutr  27411  negsproplem4  27505  negsproplem5  27506  negsproplem6  27507  precsexlem11  27663  axlowdimlem3  28202  axlowdimlem7  28206  axlowdimlem16  28215  axlowdim  28219  umgr2v2e  28782  clwlkclwwlken  29265  clwwlken  29305  0wlkonlem2  29372  clwwlknonclwlknonen  29616  dlwwlknondlwlknonen  29619  eulerpartlemgvv  33375  lfuhgr2  34109  poimirlem26  36514  mblfinlem2  36526  itg2addnclem3  36541  pr2cv  42299  isosctrlem1ALT  43695  fmtnorec1  46205  evengpoap3  46467  line2x  47440  icccldii  47551