Theorem mp3an12i 1464

Description: mp3an 1460 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 1450	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  csbwrecsg  8122  oneo  8389  nnneo  8460  ener  8762  unxpdomlem3  8999  dfac2b  9879  ackbij2  9992  axgroth3  10580  mul02  11145  recreclt  11866  cju  11961  elnnnn0c  12270  elnnz1  12338  eluzsubi  12603  uz3m2nn  12622  iccen  13220  mptnn0fsupp  13707  hashgt23el  14129  hashfun  14142  hashf1lem1  14158  hashf1lem1OLD  14159  funcnvs2  14616  remim  14818  iseraltlem2  15384  climcndslem1  15551  geo2lim  15577  fprodge0  15693  fprodge1  15695  absefib  15897  efieq1re  15898  3dvds  16030  oddp1d2  16057  bitsres  16170  phiprmpw  16467  pythagtriplem1  16507  symggen  19068  psgnuni  19097  lt6abl  19486  pws1  19845  0ringnnzr  20530  pmatcollpw2lem  21916  uzrest  23038  ressuss  23404  reperflem  23971  xrge0tsms  23987  cphsqrtcl  24338  ovolicopnf  24678  itg2seq  24897  itg2monolem2  24906  itgz  24935  ibl0  24941  iblss  24959  itgeqa  24968  iblconst  24972  iblabsr  24984  iblmulc2  24985  itgsplit  24990  tdeglem4  25214  tdeglem4OLD  25215  dvnply2  25437  aannenlem2  25479  aannenlem3  25480  aalioulem2  25483  aaliou3lem2  25493  psercn  25575  abelth  25590  pilem3  25602  resinf1o  25682  efif1olem4  25691  logdivlti  25765  dvlog2lem  25797  efopn  25803  cxpsqrt  25848  isosctrlem1  25958  asinsin  26032  atanlogsub  26056  atanbnd  26066  atantayl2  26078  basellem2  26221  basellem3  26222  isnsqf  26274  ppidif  26302  1sgm2ppw  26338  ppiublem1  26340  bposlem6  26427  bposlem9  26430  gausslemma2dlem1  26504  lgseisenlem1  26513  lgseisen  26517  lgsquad3  26525  m1lgs  26526  ostth3  26776  axlowdimlem3  27302  axlowdimlem7  27306  axlowdimlem16  27315  axlowdim  27319  umgr2v2e  27882  clwlkclwwlken  28364  clwwlken  28404  0wlkonlem2  28471  clwwlknonclwlknonen  28715  dlwwlknondlwlknonen  28718  eulerpartlemgvv  32331  lfuhgr2  33068  naddcllem  33819  scutbdaybnd  33997  scutbdaybnd2  33998  scutbdaylt  34000  madebdaylemlrcut  34067  cofcut1  34078  cofcutr  34080  poimirlem26  35791  mblfinlem2  35803  itg2addnclem3  35818  pr2cv  41117  isosctrlem1ALT  42516  fmtnorec1  44950  evengpoap3  45212  line2x  46061  icccldii  46173