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  8297  oneo  8545  nnneo  8619  naddcllem  8640  ener  8972  sucdom2  9167  unxpdomlem3  9199  dfac2b  10084  ackbij2  10195  axgroth3  10784  mul02  11352  recreclt  12082  cju  12182  elnnnn0c  12487  elnnz1  12559  eluzsubiOLD  12827  uz3m2nn  12853  iccen  13458  mptnn0fsupp  13962  hashgt23el  14389  hashfun  14402  hashf1lem1  14420  hash7g  14451  hash3tpexb  14459  funcnvs2  14879  remim  15083  iseraltlem2  15649  climcndslem1  15815  geo2lim  15841  fprodge0  15959  fprodge1  15961  absefib  16166  efieq1re  16167  3dvds  16301  oddp1d2  16328  bitsres  16443  phiprmpw  16746  pythagtriplem1  16787  symggen  19400  psgnuni  19429  lt6abl  19825  pws1  20234  0ringnnzr  20434  pmatcollpw2lem  22664  uzrest  23784  ressuss  24150  reperflem  24707  xrge0tsms  24723  cphsqrtcl  25084  ovolicopnf  25425  itg2seq  25643  itg2monolem2  25652  itgz  25682  ibl0  25688  iblss  25706  itgeqa  25715  iblconst  25719  iblabsr  25731  iblmulc2  25732  itgsplit  25737  tdeglem4  25965  dvnply2  26195  aannenlem2  26237  aannenlem3  26238  aalioulem2  26241  aaliou3lem2  26251  psercn  26336  abelth  26351  pilem3  26363  resinf1o  26445  efif1olem4  26454  logdivlti  26529  dvlog2lem  26561  efopn  26567  cxpsqrt  26612  isosctrlem1  26728  asinsin  26802  atanlogsub  26826  atanbnd  26836  atantayl2  26848  basellem2  26992  basellem3  26993  isnsqf  27045  ppidif  27073  1sgm2ppw  27111  ppiublem1  27113  bposlem6  27200  bposlem9  27203  gausslemma2dlem1  27277  lgseisenlem1  27286  lgseisen  27290  lgsquad3  27298  m1lgs  27299  ostth3  27549  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  negsproplem4  27937  negsproplem5  27938  negsproplem6  27939  precsexlem11  28119  pw2divscld  28324  pw2divsmuld  28325  pw2divscan2d  28327  pw2divsrecd  28330  axlowdimlem3  28871  axlowdimlem7  28875  axlowdimlem16  28884  axlowdim  28888  umgr2v2e  29453  clwlkclwwlken  29941  clwwlken  29981  0wlkonlem2  30048  clwwlknonclwlknonen  30292  dlwwlknondlwlknonen  30295  eulerpartlemgvv  34367  lfuhgr2  35106  poimirlem26  37640  mblfinlem2  37652  itg2addnclem3  37667  pr2cv  43537  isosctrlem1ALT  44923  fmtnorec1  47535  evengpoap3  47797  pgnioedg1  48095  pgnioedg2  48096  pgnioedg3  48097  pgnioedg4  48098  pgnioedg5  48099  pgnbgreunbgrlem2lem1  48101  pgnbgreunbgrlem2lem2  48102  pgnbgreunbgrlem5lem1  48107  pgnbgreunbgrlem5lem2  48108  pgnbgreunbgrlem5lem3  48109  line2x  48740  icccldii  48904