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 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  csbwrecsg  8275  oneo  8523  nnneo  8597  naddcllem  8618  ener  8950  sucdom2  9145  unxpdomlem3  9176  dfac2b  10063  ackbij2  10174  axgroth3  10763  mul02  11331  recreclt  12061  cju  12161  elnnnn0c  12466  elnnz1  12538  eluzsubiOLD  12806  uz3m2nn  12832  iccen  13437  mptnn0fsupp  13941  hashgt23el  14368  hashfun  14381  hashf1lem1  14399  hash7g  14430  hash3tpexb  14438  funcnvs2  14857  remim  15061  iseraltlem2  15627  climcndslem1  15793  geo2lim  15819  fprodge0  15937  fprodge1  15939  absefib  16144  efieq1re  16145  3dvds  16279  oddp1d2  16306  bitsres  16421  phiprmpw  16724  pythagtriplem1  16765  symggen  19386  psgnuni  19415  lt6abl  19811  pws1  20247  0ringnnzr  20447  pmatcollpw2lem  22699  uzrest  23819  ressuss  24185  reperflem  24742  xrge0tsms  24758  cphsqrtcl  25119  ovolicopnf  25460  itg2seq  25678  itg2monolem2  25687  itgz  25717  ibl0  25723  iblss  25741  itgeqa  25750  iblconst  25754  iblabsr  25766  iblmulc2  25767  itgsplit  25772  tdeglem4  26000  dvnply2  26230  aannenlem2  26272  aannenlem3  26273  aalioulem2  26276  aaliou3lem2  26286  psercn  26371  abelth  26386  pilem3  26398  resinf1o  26480  efif1olem4  26489  logdivlti  26564  dvlog2lem  26596  efopn  26602  cxpsqrt  26647  isosctrlem1  26763  asinsin  26837  atanlogsub  26861  atanbnd  26871  atantayl2  26883  basellem2  27027  basellem3  27028  isnsqf  27080  ppidif  27108  1sgm2ppw  27146  ppiublem1  27148  bposlem6  27235  bposlem9  27238  gausslemma2dlem1  27312  lgseisenlem1  27321  lgseisen  27325  lgsquad3  27333  m1lgs  27334  ostth3  27584  scutbdaybnd  27763  scutbdaybnd2  27764  scutbdaylt  27766  madebdaylemlrcut  27850  bdayiun  27866  cofcut1  27870  cofcutr  27874  negsproplem4  27979  negsproplem5  27980  negsproplem6  27981  precsexlem11  28161  pw2divscld  28368  pw2divsmuld  28369  pw2divscan2d  28371  pw2divsassd  28372  pw2divsrecd  28376  zs12zodd  28396  axlowdimlem3  28926  axlowdimlem7  28930  axlowdimlem16  28939  axlowdim  28943  umgr2v2e  29508  clwlkclwwlken  29993  clwwlken  30033  0wlkonlem2  30100  clwwlknonclwlknonen  30344  dlwwlknondlwlknonen  30347  eulerpartlemgvv  34362  lfuhgr2  35101  poimirlem26  37635  mblfinlem2  37647  itg2addnclem3  37662  pr2cv  43532  isosctrlem1ALT  44918  fmtnorec1  47533  evengpoap3  47795  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  line2x  48738  icccldii  48902