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  8248  oneo  8496  nnneo  8570  naddcllem  8591  ener  8923  sucdom2  9112  unxpdomlem3  9142  dfac2b  10022  ackbij2  10133  axgroth3  10722  mul02  11291  recreclt  12021  cju  12121  elnnnn0c  12426  elnnz1  12498  eluzsubiOLD  12766  uz3m2nn  12792  iccen  13397  mptnn0fsupp  13904  hashgt23el  14331  hashfun  14344  hashf1lem1  14362  hash7g  14393  hash3tpexb  14401  funcnvs2  14820  remim  15024  iseraltlem2  15590  climcndslem1  15756  geo2lim  15782  fprodge0  15900  fprodge1  15902  absefib  16107  efieq1re  16108  3dvds  16242  oddp1d2  16269  bitsres  16384  phiprmpw  16687  pythagtriplem1  16728  symggen  19382  psgnuni  19411  lt6abl  19807  pws1  20243  0ringnnzr  20440  pmatcollpw2lem  22692  uzrest  23812  ressuss  24177  reperflem  24734  xrge0tsms  24750  cphsqrtcl  25111  ovolicopnf  25452  itg2seq  25670  itg2monolem2  25679  itgz  25709  ibl0  25715  iblss  25733  itgeqa  25742  iblconst  25746  iblabsr  25758  iblmulc2  25759  itgsplit  25764  tdeglem4  25992  dvnply2  26222  aannenlem2  26264  aannenlem3  26265  aalioulem2  26268  aaliou3lem2  26278  psercn  26363  abelth  26378  pilem3  26390  resinf1o  26472  efif1olem4  26481  logdivlti  26556  dvlog2lem  26588  efopn  26594  cxpsqrt  26639  isosctrlem1  26755  asinsin  26829  atanlogsub  26853  atanbnd  26863  atantayl2  26875  basellem2  27019  basellem3  27020  isnsqf  27072  ppidif  27100  1sgm2ppw  27138  ppiublem1  27140  bposlem6  27227  bposlem9  27230  gausslemma2dlem1  27304  lgseisenlem1  27313  lgseisen  27317  lgsquad3  27325  m1lgs  27326  ostth3  27576  scutbdaybnd  27756  scutbdaybnd2  27757  scutbdaylt  27759  madebdaylemlrcut  27844  bdayiun  27860  cofcut1  27864  cofcutr  27868  negsproplem4  27973  negsproplem5  27974  negsproplem6  27975  precsexlem11  28155  pw2divscld  28362  pw2divsmuld  28363  pw2divscan2d  28365  pw2divsassd  28366  pw2divsrecd  28370  zs12zodd  28392  axlowdimlem3  28922  axlowdimlem7  28926  axlowdimlem16  28935  axlowdim  28939  umgr2v2e  29504  clwlkclwwlken  29992  clwwlken  30032  0wlkonlem2  30099  clwwlknonclwlknonen  30343  dlwwlknondlwlknonen  30346  eulerpartlemgvv  34389  lfuhgr2  35163  poimirlem26  37685  mblfinlem2  37697  itg2addnclem3  37712  pr2cv  43640  isosctrlem1ALT  45025  fmtnorec1  47636  evengpoap3  47898  pgnioedg1  48207  pgnioedg2  48208  pgnioedg3  48209  pgnioedg4  48210  pgnioedg5  48211  pgnbgreunbgrlem2lem1  48213  pgnbgreunbgrlem2lem2  48214  pgnbgreunbgrlem5lem1  48219  pgnbgreunbgrlem5lem2  48220  pgnbgreunbgrlem5lem3  48221  line2x  48854  icccldii  49018