Theorem mp3an12i 1494

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  csbwrecsg  8336  oneo  8589  nnneo  8664  naddcllem  8685  ener  9028  sucdom2  9218  unxpdomlem3  9249  dfac2b  10209  ackbij2  10320  axgroth3  10916  mul02  11488  recreclt  12216  cju  12316  elnnnn0c  12651  elnnz1  12722  uz3m2nn  13021  iccen  13628  mptnn0fsupp  14140  hashgt23el  14569  hashfun  14582  hashf1lem1  14600  hash7g  14631  hash3tpexb  14639  funcnvs2  15064  remim  15284  iseraltlem2  15850  climcndslem1  16018  geo2lim  16044  fprodge0  16160  fprodge1  16162  absefib  16366  efieq1re  16367  3dvds  16501  oddp1d2  16528  bitsres  16643  phiprmpw  16953  pythagtriplem1  16994  symggen  19684  psgnuni  19713  lt6abl  20109  pws1  20554  0ringnnzr  20776  pmatcollpw2lem  23095  uzrest  24216  ressuss  24581  reperflem  25138  xrge0tsms  25154  cphsqrtcl  25505  ovolicopnf  25845  itg2seq  26063  itg2monolem2  26072  itgz  26101  ibl0  26107  iblss  26125  itgeqa  26134  iblconst  26138  iblabsr  26150  iblmulc2  26151  itgsplit  26156  tdeglem4  26378  dvnply2  26608  aannenlem2  26656  aannenlem3  26657  aalioulem2  26660  aaliou3lem2  26670  psercn  26753  abelth  26768  pilem3  26780  resinf1o  26864  efif1olem4  26873  logdivlti  26948  dvlog2lem  26980  efopn  26986  cxpsqrt  27031  isosctrlem1  27146  asinsin  27220  atanlogsub  27244  atanbnd  27254  atantayl2  27266  basellem2  27409  basellem3  27410  isnsqf  27462  ppidif  27490  1sgm2ppw  27527  ppiublem1  27529  bposlem6  27616  bposlem9  27619  gausslemma2dlem1  27693  lgseisenlem1  27702  lgseisen  27706  lgsquad3  27714  m1lgs  27715  ostth3  27965  fltoprmlem2  27994  cutbdaybnd  28181  cutbdaybnd2  28182  cutbdaylt  28184  madebdaylemlrcut  28285  bdayiun  28301  sltsbday  28303  cofcut1  28306  cofcutr  28310  negsproplem4  28417  negsproplem5  28418  negsproplem6  28419  precsexlem11  28603  pw2divscld  28825  pw2divmulsd  28826  pw2divscan2d  28828  pw2divsassd  28829  pw2divsrecd  28833  bdayfinbndlem1  28853  z12zsodd  28868  axlowdimlem3  29522  axlowdimlem7  29526  axlowdimlem16  29535  axlowdim  29539  lfuhgr2  29727  umgr2v2e  30106  clwlkclwwlken  30603  clwwlken  30643  0wlkonlem2  30710  clwwlknonclwlknonen  30964  dlwwlknondlwlknonen  30967  eulerpartlemgvv  35008  nmulprop  36939  poimirlem26  38565  mblfinlem2  38577  itg2addnclem3  38592  pr2cv  44549  isosctrlem1ALT  45916  fourierdlem48  47164  fourierdlem49  47165  fourierdlem113  47229  muldvdsfacgt  48456  fmtnorec1  48622  evengpoap3  48897  pgnioedg1  49206  pgnioedg2  49207  pgnioedg3  49208  pgnioedg4  49209  pgnioedg5  49210  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem5lem1  49218  pgnbgreunbgrlem5lem2  49219  pgnbgreunbgrlem5lem3  49220  line2x  49866  icccldii  50027