Theorem mp3an12i 1465

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  csbwrecsg  8362  oneo  8637  nnneo  8711  naddcllem  8732  ener  9061  sucdom2  9269  unxpdomlem3  9315  dfac2b  10200  ackbij2  10311  axgroth3  10900  mul02  11468  recreclt  12194  cju  12289  elnnnn0c  12598  elnnz1  12669  eluzsubiOLD  12937  uz3m2nn  12956  iccen  13557  mptnn0fsupp  14048  hashgt23el  14473  hashfun  14486  hashf1lem1  14504  hash7g  14535  hash3tpexb  14543  funcnvs2  14962  remim  15166  iseraltlem2  15731  climcndslem1  15897  geo2lim  15923  fprodge0  16041  fprodge1  16043  absefib  16246  efieq1re  16247  3dvds  16379  oddp1d2  16406  bitsres  16519  phiprmpw  16823  pythagtriplem1  16863  symggen  19512  psgnuni  19541  lt6abl  19937  pws1  20348  0ringnnzr  20551  pmatcollpw2lem  22804  uzrest  23926  ressuss  24292  reperflem  24859  xrge0tsms  24875  cphsqrtcl  25237  ovolicopnf  25578  itg2seq  25797  itg2monolem2  25806  itgz  25836  ibl0  25842  iblss  25860  itgeqa  25869  iblconst  25873  iblabsr  25885  iblmulc2  25886  itgsplit  25891  tdeglem4  26119  dvnply2  26347  aannenlem2  26389  aannenlem3  26390  aalioulem2  26393  aaliou3lem2  26403  psercn  26488  abelth  26503  pilem3  26515  resinf1o  26596  efif1olem4  26605  logdivlti  26680  dvlog2lem  26712  efopn  26718  cxpsqrt  26763  isosctrlem1  26879  asinsin  26953  atanlogsub  26977  atanbnd  26987  atantayl2  26999  basellem2  27143  basellem3  27144  isnsqf  27196  ppidif  27224  1sgm2ppw  27262  ppiublem1  27264  bposlem6  27351  bposlem9  27354  gausslemma2dlem1  27428  lgseisenlem1  27437  lgseisen  27441  lgsquad3  27449  m1lgs  27450  ostth3  27700  scutbdaybnd  27878  scutbdaybnd2  27879  scutbdaylt  27881  madebdaylemlrcut  27955  cofcut1  27972  cofcutr  27976  negsproplem4  28081  negsproplem5  28082  negsproplem6  28083  precsexlem11  28259  axlowdimlem3  28977  axlowdimlem7  28981  axlowdimlem16  28990  axlowdim  28994  umgr2v2e  29561  clwlkclwwlken  30044  clwwlken  30084  0wlkonlem2  30151  clwwlknonclwlknonen  30395  dlwwlknondlwlknonen  30398  eulerpartlemgvv  34341  lfuhgr2  35086  poimirlem26  37606  mblfinlem2  37618  itg2addnclem3  37633  pr2cv  43510  isosctrlem1ALT  44905  fmtnorec1  47411  evengpoap3  47673  line2x  48488  icccldii  48598