Theorem mp3an12i 1463

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  csbwrecsg  8308  oneo  8583  nnneo  8656  naddcllem  8677  ener  8999  sucdom2  9208  unxpdomlem3  9254  dfac2b  10127  ackbij2  10240  axgroth3  10828  mul02  11396  recreclt  12117  cju  12212  elnnnn0c  12521  elnnz1  12592  eluzsubiOLD  12860  uz3m2nn  12879  iccen  13478  mptnn0fsupp  13966  hashgt23el  14388  hashfun  14401  hashf1lem1  14419  hashf1lem1OLD  14420  funcnvs2  14868  remim  15068  iseraltlem2  15633  climcndslem1  15799  geo2lim  15825  fprodge0  15941  fprodge1  15943  absefib  16145  efieq1re  16146  3dvds  16278  oddp1d2  16305  bitsres  16418  phiprmpw  16713  pythagtriplem1  16753  symggen  19379  psgnuni  19408  lt6abl  19804  pws1  20213  0ringnnzr  20414  pmatcollpw2lem  22499  uzrest  23621  ressuss  23987  reperflem  24554  xrge0tsms  24570  cphsqrtcl  24932  ovolicopnf  25273  itg2seq  25492  itg2monolem2  25501  itgz  25530  ibl0  25536  iblss  25554  itgeqa  25563  iblconst  25567  iblabsr  25579  iblmulc2  25580  itgsplit  25585  tdeglem4  25812  tdeglem4OLD  25813  dvnply2  26036  aannenlem2  26078  aannenlem3  26079  aalioulem2  26082  aaliou3lem2  26092  psercn  26174  abelth  26189  pilem3  26201  resinf1o  26281  efif1olem4  26290  logdivlti  26364  dvlog2lem  26396  efopn  26402  cxpsqrt  26447  isosctrlem1  26559  asinsin  26633  atanlogsub  26657  atanbnd  26667  atantayl2  26679  basellem2  26822  basellem3  26823  isnsqf  26875  ppidif  26903  1sgm2ppw  26939  ppiublem1  26941  bposlem6  27028  bposlem9  27031  gausslemma2dlem1  27105  lgseisenlem1  27114  lgseisen  27118  lgsquad3  27126  m1lgs  27127  ostth3  27377  scutbdaybnd  27553  scutbdaybnd2  27554  scutbdaylt  27556  madebdaylemlrcut  27630  cofcut1  27645  cofcutr  27649  negsproplem4  27744  negsproplem5  27745  negsproplem6  27746  precsexlem11  27902  axlowdimlem3  28469  axlowdimlem7  28473  axlowdimlem16  28482  axlowdim  28486  umgr2v2e  29049  clwlkclwwlken  29532  clwwlken  29572  0wlkonlem2  29639  clwwlknonclwlknonen  29883  dlwwlknondlwlknonen  29886  eulerpartlemgvv  33673  lfuhgr2  34407  poimirlem26  36817  mblfinlem2  36829  itg2addnclem3  36844  pr2cv  42601  isosctrlem1ALT  43997  fmtnorec1  46503  evengpoap3  46765  line2x  47527  icccldii  47638