Theorem mp3an13 1482

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an13.1	⊢ 𝜑
mp3an13.2	⊢ 𝜒
mp3an13.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an13	⊢ (𝜓 → 𝜃)

Proof of Theorem mp3an13

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 ⊢ 𝜑
2		mp3an13.2	. . 3 ⊢ 𝜒
3		mp3an13.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1480	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  predeq2  6322  wrecseq2  8359  oeoalem  8630  mulrid  11330  addltmul  12606  fz01en  13710  fznatpl1  13736  expubnd  14345  bernneq  14397  bernneq2  14398  faclbnd4lem1  14461  hashfun  14606  bpoly2  16249  bpoly3  16250  fsumcube  16252  efi4p  16331  efival  16346  cos2tsin  16373  cos01bnd  16380  cos01gt0  16385  dvds0  16467  odd2np1  16537  opoe  16559  divalglem0  16589  gcdid  16725  pythagtriplem4  17023  ressid  17448  fvpr0o  17757  fvpr1o  17758  zringcyg  21802  lecldbas  23564  blssioo  25141  tgioo  25142  rerest  25150  xrrest  25154  zdis  25163  reconnlem2  25174  metdscn2  25204  negcncf  25270  iihalf2  25281  cncmet  25670  rrxmvallem  25752  rrxmval  25753  ovolunlem1a  25844  ismbf3d  26002  c1lip2  26345  pilem2  26806  pilem3  26807  sinperlem  26836  sincosq1sgn  26854  sincosq2sgn  26855  sinq12gt0  26863  cosq14gt0  26866  cosq14ge0  26867  coseq1  26880  sinord  26889  zetacvg  27369  1sgmprm  27553  ppiub  27558  chtublem  27565  chtub  27566  bcp1ctr  27633  bpos1lem  27636  bposlem2  27639  bposlem3  27640  bposlem4  27641  bposlem5  27642  bposlem6  27643  bposlem7  27644  bposlem9  27646  nnsge1  28756  pw2gt0divsd  28858  pw2ge0divsd  28859  pw2ltdivmulsd  28863  pw2ltmuldivs2d  28864  pw2ltdivmuls2d  28870  pw2cut  28873  bdayfinbndlem1  28880  axlowdim  29566  ipidsq  31339  ipasslem1  31460  ipasslem2  31461  ipasslem4  31463  ipasslem5  31464  ipasslem8  31466  ipasslem9  31467  ipasslem11  31469  pjoc1i  32060  h1de2bi  32183  h1de2ctlem  32184  spanunsni  32208  opsqrlem1  32769  opsqrlem6  32774  chrelati  32993  chrelat2i  32994  cvexchlem  32997  pnfinf  33811  1fldgenq  33951  rrhre  34720  jf1o  36010  erdszelem5  36126  wsuceq2  36755  taupilem1  38433  finxpreclem2  38504  sin2h  38724  cos2h  38725  tan2h  38726  poimirlem27  38756  poimirlem30  38759  broucube  38763  mblfinlem1  38766  heiborlem6  38941  lcmineqlem19  43288  onexomgt  44433  omabs2  44524  icccncfext  47100  dirkertrigeq  47314  pgnbgreunbgrlem4  49420  zlmodzxzel  49670  dignn0flhalflem1  49930  2arymaptfo  49969  fv1prop  50014  fv2prop  50015  onetansqsecsq  51132  cotsqcscsq  51133