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  8320  oneo  8571  nnneo  8646  naddcllem  8667  ener  9010  sucdom2  9200  unxpdomlem3  9231  dfac2b  10136  ackbij2  10247  axgroth3  10843  mul02  11415  recreclt  12141  cju  12241  elnnnn0c  12576  elnnz1  12647  uz3m2nn  12946  iccen  13552  mptnn0fsupp  14063  hashgt23el  14491  hashfun  14504  hashf1lem1  14522  hash7g  14553  hash3tpexb  14561  funcnvs2  14986  remim  15206  iseraltlem2  15772  climcndslem1  15940  geo2lim  15966  fprodge0  16084  fprodge1  16086  absefib  16290  efieq1re  16291  3dvds  16425  oddp1d2  16452  bitsres  16567  phiprmpw  16871  pythagtriplem1  16912  symggen  19598  psgnuni  19627  lt6abl  20023  pws1  20466  0ringnnzr  20687  pmatcollpw2lem  23003  uzrest  24124  ressuss  24489  reperflem  25046  xrge0tsms  25062  cphsqrtcl  25413  ovolicopnf  25753  itg2seq  25971  itg2monolem2  25980  itgz  26010  ibl0  26016  iblss  26034  itgeqa  26043  iblconst  26047  iblabsr  26059  iblmulc2  26060  itgsplit  26065  tdeglem4  26287  dvnply2  26518  aannenlem2  26562  aannenlem3  26563  aalioulem2  26566  aaliou3lem2  26576  psercn  26659  abelth  26674  pilem3  26686  resinf1o  26771  efif1olem4  26780  logdivlti  26855  dvlog2lem  26887  efopn  26893  cxpsqrt  26938  isosctrlem1  27053  asinsin  27127  atanlogsub  27151  atanbnd  27161  atantayl2  27173  basellem2  27316  basellem3  27317  isnsqf  27369  ppidif  27397  1sgm2ppw  27434  ppiublem1  27436  bposlem6  27523  bposlem9  27526  gausslemma2dlem1  27600  lgseisenlem1  27609  lgseisen  27613  lgsquad3  27621  m1lgs  27622  ostth3  27872  cutbdaybnd  28058  cutbdaybnd2  28059  cutbdaylt  28061  madebdaylemlrcut  28162  bdayiun  28178  sltsbday  28180  cofcut1  28183  cofcutr  28187  negsproplem4  28294  negsproplem5  28295  negsproplem6  28296  precsexlem11  28480  pw2divscld  28702  pw2divmulsd  28703  pw2divscan2d  28705  pw2divsassd  28706  pw2divsrecd  28710  bdayfinbndlem1  28730  z12zsodd  28745  axlowdimlem3  29387  axlowdimlem7  29391  axlowdimlem16  29400  axlowdim  29404  lfuhgr2  29592  umgr2v2e  29971  clwlkclwwlken  30468  clwwlken  30508  0wlkonlem2  30575  clwwlknonclwlknonen  30829  dlwwlknondlwlknonen  30832  eulerpartlemgvv  34874  nmulprop  36757  poimirlem26  38382  mblfinlem2  38394  itg2addnclem3  38409  pr2cv  44375  isosctrlem1ALT  45743  fourierdlem48  46969  fourierdlem49  46970  fourierdlem113  47034  muldvdsfacgt  48261  fmtnorec1  48427  evengpoap3  48702  pgnioedg1  49011  pgnioedg2  49012  pgnioedg3  49013  pgnioedg4  49014  pgnioedg5  49015  pgnbgreunbgrlem2lem1  49017  pgnbgreunbgrlem2lem2  49018  pgnbgreunbgrlem5lem1  49023  pgnbgreunbgrlem5lem2  49024  pgnbgreunbgrlem5lem3  49025  line2x  49671  icccldii  49832