Theorem mp3an12i 1461

Description: mp3an 1457 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 1447	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oneo  8210  nnneo  8281  ener  8559  unxpdomlem3  8727  dfac2b  9559  ackbij2  9668  axgroth3  10256  mul02  10821  recreclt  11542  cju  11637  elnnnn0c  11945  elnnz1  12011  eluzsubi  12275  uz3m2nn  12294  iccen  12886  mptnn0fsupp  13368  hashgt23el  13788  hashfun  13801  hashf1lem1  13816  funcnvs2  14278  remim  14479  iseraltlem2  15042  climcndslem1  15207  geo2lim  15234  fprodge0  15350  fprodge1  15352  absefib  15554  efieq1re  15555  3dvds  15683  oddp1d2  15710  bitsres  15825  phiprmpw  16116  pythagtriplem1  16156  symggen  18601  psgnuni  18630  lt6abl  19018  pws1  19369  0ringnnzr  20045  pmatcollpw2lem  21388  uzrest  22508  ressuss  22875  reperflem  23429  xrge0tsms  23445  cphsqrtcl  23791  ovolicopnf  24128  itg2seq  24346  itg2monolem2  24355  itgz  24384  ibl0  24390  iblss  24408  itgeqa  24417  iblconst  24421  iblabsr  24433  iblmulc2  24434  itgsplit  24439  tdeglem4  24657  dvnply2  24879  aannenlem2  24921  aannenlem3  24922  aalioulem2  24925  aaliou3lem2  24935  psercn  25017  abelth  25032  pilem3  25044  resinf1o  25123  efif1olem4  25132  logdivlti  25206  dvlog2lem  25238  efopn  25244  cxpsqrt  25289  isosctrlem1  25399  asinsin  25473  atanlogsub  25497  atanbnd  25507  atantayl2  25519  basellem2  25662  basellem3  25663  isnsqf  25715  ppidif  25743  1sgm2ppw  25779  ppiublem1  25781  bposlem6  25868  bposlem9  25871  gausslemma2dlem1  25945  lgseisenlem1  25954  lgseisen  25958  lgsquad3  25966  m1lgs  25967  ostth3  26217  axlowdimlem3  26733  axlowdimlem7  26737  axlowdimlem16  26746  axlowdim  26750  umgr2v2e  27310  clwlkclwwlken  27793  clwwlken  27834  0wlkonlem2  27901  clwwlknonclwlknonen  28145  dlwwlknondlwlknonen  28148  eulerpartlemgvv  31638  lfuhgr2  32369  scutbdaybnd  33279  scutbdaylt  33280  poimirlem26  34922  mblfinlem2  34934  pr2cv  39913  isosctrlem1ALT  41274  fmtnorec1  43706  evengpoap3  43971  line2x  44748