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  8315  oneo  8568  nnneo  8643  naddcllem  8664  ener  9007  sucdom2  9197  unxpdomlem3  9228  dfac2b  10166  ackbij2  10277  axgroth3  10873  mul02  11445  recreclt  12171  cju  12271  elnnnn0c  12606  elnnz1  12677  uz3m2nn  12976  iccen  13583  mptnn0fsupp  14094  hashgt23el  14522  hashfun  14535  hashf1lem1  14553  hash7g  14584  hash3tpexb  14592  funcnvs2  15017  remim  15237  iseraltlem2  15803  climcndslem1  15971  geo2lim  15997  fprodge0  16113  fprodge1  16115  absefib  16319  efieq1re  16320  3dvds  16454  oddp1d2  16481  bitsres  16596  phiprmpw  16900  pythagtriplem1  16941  symggen  19631  psgnuni  19660  lt6abl  20056  pws1  20501  0ringnnzr  20723  pmatcollpw2lem  23042  uzrest  24163  ressuss  24528  reperflem  25085  xrge0tsms  25101  cphsqrtcl  25452  ovolicopnf  25792  itg2seq  26010  itg2monolem2  26019  itgz  26048  ibl0  26054  iblss  26072  itgeqa  26081  iblconst  26085  iblabsr  26097  iblmulc2  26098  itgsplit  26103  tdeglem4  26325  dvnply2  26557  aannenlem2  26605  aannenlem3  26606  aalioulem2  26609  aaliou3lem2  26619  psercn  26702  abelth  26717  pilem3  26729  resinf1o  26813  efif1olem4  26822  logdivlti  26897  dvlog2lem  26929  efopn  26935  cxpsqrt  26980  isosctrlem1  27095  asinsin  27169  atanlogsub  27193  atanbnd  27203  atantayl2  27215  basellem2  27358  basellem3  27359  isnsqf  27411  ppidif  27439  1sgm2ppw  27476  ppiublem1  27478  bposlem6  27565  bposlem9  27568  gausslemma2dlem1  27642  lgseisenlem1  27651  lgseisen  27655  lgsquad3  27663  m1lgs  27664  ostth3  27914  cutbdaybnd  28100  cutbdaybnd2  28101  cutbdaylt  28103  madebdaylemlrcut  28204  bdayiun  28220  sltsbday  28222  cofcut1  28225  cofcutr  28229  negsproplem4  28336  negsproplem5  28337  negsproplem6  28338  precsexlem11  28522  pw2divscld  28744  pw2divmulsd  28745  pw2divscan2d  28747  pw2divsassd  28748  pw2divsrecd  28752  bdayfinbndlem1  28772  z12zsodd  28787  axlowdimlem3  29441  axlowdimlem7  29445  axlowdimlem16  29454  axlowdim  29458  lfuhgr2  29646  umgr2v2e  30025  clwlkclwwlken  30522  clwwlken  30562  0wlkonlem2  30629  clwwlknonclwlknonen  30883  dlwwlknondlwlknonen  30886  eulerpartlemgvv  34928  nmulprop  36855  poimirlem26  38478  mblfinlem2  38490  itg2addnclem3  38505  pr2cv  44486  isosctrlem1ALT  45854  fourierdlem48  47080  fourierdlem49  47081  fourierdlem113  47145  muldvdsfacgt  48372  fmtnorec1  48538  evengpoap3  48813  pgnioedg1  49122  pgnioedg2  49123  pgnioedg3  49124  pgnioedg4  49125  pgnioedg5  49126  pgnbgreunbgrlem2lem1  49128  pgnbgreunbgrlem2lem2  49129  pgnbgreunbgrlem5lem1  49134  pgnbgreunbgrlem5lem2  49135  pgnbgreunbgrlem5lem3  49136  line2x  49782  icccldii  49943