Theorem mp3an12i 1468

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  csbwrecsg  8272  oneo  8520  nnneo  8595  naddcllem  8616  ener  8952  sucdom2  9141  unxpdomlem3  9172  dfac2b  10055  ackbij2  10166  axgroth3  10756  mul02  11325  recreclt  12055  cju  12155  elnnnn0c  12460  elnnz1  12531  uz3m2nn  12821  iccen  13427  mptnn0fsupp  13934  hashgt23el  14361  hashfun  14374  hashf1lem1  14392  hash7g  14423  hash3tpexb  14431  funcnvs2  14850  remim  15054  iseraltlem2  15620  climcndslem1  15786  geo2lim  15812  fprodge0  15930  fprodge1  15932  absefib  16137  efieq1re  16138  3dvds  16272  oddp1d2  16299  bitsres  16414  phiprmpw  16717  pythagtriplem1  16758  symggen  19416  psgnuni  19445  lt6abl  19841  pws1  20277  0ringnnzr  20475  pmatcollpw2lem  22738  uzrest  23858  ressuss  24223  reperflem  24780  xrge0tsms  24796  cphsqrtcl  25157  ovolicopnf  25498  itg2seq  25716  itg2monolem2  25725  itgz  25755  ibl0  25761  iblss  25779  itgeqa  25788  iblconst  25792  iblabsr  25804  iblmulc2  25805  itgsplit  25810  tdeglem4  26038  dvnply2  26268  aannenlem2  26310  aannenlem3  26311  aalioulem2  26314  aaliou3lem2  26324  psercn  26409  abelth  26424  pilem3  26436  resinf1o  26518  efif1olem4  26527  logdivlti  26602  dvlog2lem  26634  efopn  26640  cxpsqrt  26685  isosctrlem1  26801  asinsin  26875  atanlogsub  26899  atanbnd  26909  atantayl2  26921  basellem2  27065  basellem3  27066  isnsqf  27118  ppidif  27146  1sgm2ppw  27184  ppiublem1  27186  bposlem6  27273  bposlem9  27276  gausslemma2dlem1  27350  lgseisenlem1  27359  lgseisen  27363  lgsquad3  27371  m1lgs  27372  ostth3  27622  cutbdaybnd  27808  cutbdaybnd2  27809  cutbdaylt  27811  madebdaylemlrcut  27912  bdayiun  27928  sltsbday  27930  cofcut1  27933  cofcutr  27937  negsproplem4  28044  negsproplem5  28045  negsproplem6  28046  precsexlem11  28230  pw2divscld  28452  pw2divmulsd  28453  pw2divscan2d  28455  pw2divsassd  28456  pw2divsrecd  28460  bdayfinbndlem1  28480  z12zsodd  28495  axlowdimlem3  29035  axlowdimlem7  29039  axlowdimlem16  29048  axlowdim  29052  umgr2v2e  29617  clwlkclwwlken  30105  clwwlken  30145  0wlkonlem2  30212  clwwlknonclwlknonen  30456  dlwwlknondlwlknonen  30459  eulerpartlemgvv  34560  lfuhgr2  35341  poimirlem26  37926  mblfinlem2  37938  itg2addnclem3  37953  pr2cv  43933  isosctrlem1ALT  45318  fmtnorec1  47926  evengpoap3  48188  pgnioedg1  48497  pgnioedg2  48498  pgnioedg3  48499  pgnioedg4  48500  pgnioedg5  48501  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem5lem1  48509  pgnbgreunbgrlem5lem2  48510  pgnbgreunbgrlem5lem3  48511  line2x  49143  icccldii  49307