Theorem mp3an12i 1466

Description: mp3an 1462 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 1452	. 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  8347  oneo  8620  nnneo  8694  naddcllem  8715  ener  9042  sucdom2  9244  unxpdomlem3  9289  dfac2b  10172  ackbij2  10283  axgroth3  10872  mul02  11440  recreclt  12168  cju  12263  elnnnn0c  12573  elnnz1  12645  eluzsubiOLD  12913  uz3m2nn  12934  iccen  13538  mptnn0fsupp  14039  hashgt23el  14464  hashfun  14477  hashf1lem1  14495  hash7g  14526  hash3tpexb  14534  funcnvs2  14953  remim  15157  iseraltlem2  15720  climcndslem1  15886  geo2lim  15912  fprodge0  16030  fprodge1  16032  absefib  16235  efieq1re  16236  3dvds  16369  oddp1d2  16396  bitsres  16511  phiprmpw  16814  pythagtriplem1  16855  symggen  19489  psgnuni  19518  lt6abl  19914  pws1  20323  0ringnnzr  20526  pmatcollpw2lem  22784  uzrest  23906  ressuss  24272  reperflem  24841  xrge0tsms  24857  cphsqrtcl  25219  ovolicopnf  25560  itg2seq  25778  itg2monolem2  25787  itgz  25817  ibl0  25823  iblss  25841  itgeqa  25850  iblconst  25854  iblabsr  25866  iblmulc2  25867  itgsplit  25872  tdeglem4  26100  dvnply2  26330  aannenlem2  26372  aannenlem3  26373  aalioulem2  26376  aaliou3lem2  26386  psercn  26471  abelth  26486  pilem3  26498  resinf1o  26579  efif1olem4  26588  logdivlti  26663  dvlog2lem  26695  efopn  26701  cxpsqrt  26746  isosctrlem1  26862  asinsin  26936  atanlogsub  26960  atanbnd  26970  atantayl2  26982  basellem2  27126  basellem3  27127  isnsqf  27179  ppidif  27207  1sgm2ppw  27245  ppiublem1  27247  bposlem6  27334  bposlem9  27337  gausslemma2dlem1  27411  lgseisenlem1  27420  lgseisen  27424  lgsquad3  27432  m1lgs  27433  ostth3  27683  scutbdaybnd  27861  scutbdaybnd2  27862  scutbdaylt  27864  madebdaylemlrcut  27938  cofcut1  27955  cofcutr  27959  negsproplem4  28064  negsproplem5  28065  negsproplem6  28066  precsexlem11  28242  axlowdimlem3  28960  axlowdimlem7  28964  axlowdimlem16  28973  axlowdim  28977  umgr2v2e  29544  clwlkclwwlken  30032  clwwlken  30072  0wlkonlem2  30139  clwwlknonclwlknonen  30383  dlwwlknondlwlknonen  30386  eulerpartlemgvv  34379  lfuhgr2  35125  poimirlem26  37654  mblfinlem2  37666  itg2addnclem3  37681  pr2cv  43566  isosctrlem1ALT  44959  fmtnorec1  47529  evengpoap3  47791  line2x  48680  icccldii  48823