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

This theorem is referenced by:  csbwrecsg  8108  oneo  8374  nnneo  8445  ener  8742  unxpdomlem3  8958  dfac2b  9817  ackbij2  9930  axgroth3  10518  mul02  11083  recreclt  11804  cju  11899  elnnnn0c  12208  elnnz1  12276  eluzsubi  12541  uz3m2nn  12560  iccen  13158  mptnn0fsupp  13645  hashgt23el  14067  hashfun  14080  hashf1lem1  14096  hashf1lem1OLD  14097  funcnvs2  14554  remim  14756  iseraltlem2  15322  climcndslem1  15489  geo2lim  15515  fprodge0  15631  fprodge1  15633  absefib  15835  efieq1re  15836  3dvds  15968  oddp1d2  15995  bitsres  16108  phiprmpw  16405  pythagtriplem1  16445  symggen  18993  psgnuni  19022  lt6abl  19411  pws1  19770  0ringnnzr  20453  pmatcollpw2lem  21834  uzrest  22956  ressuss  23322  reperflem  23887  xrge0tsms  23903  cphsqrtcl  24253  ovolicopnf  24593  itg2seq  24812  itg2monolem2  24821  itgz  24850  ibl0  24856  iblss  24874  itgeqa  24883  iblconst  24887  iblabsr  24899  iblmulc2  24900  itgsplit  24905  tdeglem4  25129  tdeglem4OLD  25130  dvnply2  25352  aannenlem2  25394  aannenlem3  25395  aalioulem2  25398  aaliou3lem2  25408  psercn  25490  abelth  25505  pilem3  25517  resinf1o  25597  efif1olem4  25606  logdivlti  25680  dvlog2lem  25712  efopn  25718  cxpsqrt  25763  isosctrlem1  25873  asinsin  25947  atanlogsub  25971  atanbnd  25981  atantayl2  25993  basellem2  26136  basellem3  26137  isnsqf  26189  ppidif  26217  1sgm2ppw  26253  ppiublem1  26255  bposlem6  26342  bposlem9  26345  gausslemma2dlem1  26419  lgseisenlem1  26428  lgseisen  26432  lgsquad3  26440  m1lgs  26441  ostth3  26691  axlowdimlem3  27215  axlowdimlem7  27219  axlowdimlem16  27228  axlowdim  27232  umgr2v2e  27795  clwlkclwwlken  28277  clwwlken  28317  0wlkonlem2  28384  clwwlknonclwlknonen  28628  dlwwlknondlwlknonen  28631  eulerpartlemgvv  32243  lfuhgr2  32980  naddcllem  33758  scutbdaybnd  33936  scutbdaybnd2  33937  scutbdaylt  33939  madebdaylemlrcut  34006  cofcut1  34017  cofcutr  34019  poimirlem26  35730  mblfinlem2  35742  itg2addnclem3  35757  pr2cv  41044  isosctrlem1ALT  42443  fmtnorec1  44877  evengpoap3  45139  line2x  45988  icccldii  46100