Theorem mp3an13 1450

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 1448	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 686	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:  predeq2  6302  wrecseq2  8306  oeoalem  8598  mulrid  11216  addltmul  12452  eluzaddiOLD  12858  fz01en  13533  fznatpl1  13559  expubnd  14146  bernneq  14196  bernneq2  14197  faclbnd4lem1  14257  hashfun  14401  bpoly2  16005  bpoly3  16006  fsumcube  16008  efi4p  16084  efival  16099  cos2tsin  16126  cos01bnd  16133  cos01gt0  16138  dvds0  16219  odd2np1  16288  opoe  16310  divalglem0  16340  gcdid  16472  pythagtriplem4  16756  ressid  17193  fvpr0o  17509  fvpr1o  17510  zringcyg  21240  lecldbas  22943  blssioo  24531  tgioo  24532  rerest  24540  xrrest  24543  zdis  24552  reconnlem2  24563  metdscn2  24593  negcncf  24662  negcncfOLD  24663  iihalf2  24675  cncmet  25070  rrxmvallem  25152  rrxmval  25153  ovolunlem1a  25245  ismbf3d  25403  c1lip2  25750  pilem2  26200  pilem3  26201  sinperlem  26226  sincosq1sgn  26244  sincosq2sgn  26245  sinq12gt0  26253  cosq14gt0  26256  cosq14ge0  26257  coseq1  26270  sinord  26279  zetacvg  26755  1sgmprm  26938  ppiub  26943  chtublem  26950  chtub  26951  bcp1ctr  27018  bpos1lem  27021  bposlem2  27024  bposlem3  27025  bposlem4  27026  bposlem5  27027  bposlem6  27028  bposlem7  27029  bposlem9  27031  axlowdim  28486  ipidsq  30230  ipasslem1  30351  ipasslem2  30352  ipasslem4  30354  ipasslem5  30355  ipasslem8  30357  ipasslem9  30358  ipasslem11  30360  pjoc1i  30951  h1de2bi  31074  h1de2ctlem  31075  spanunsni  31099  opsqrlem1  31660  opsqrlem6  31665  chrelati  31884  chrelat2i  31885  cvexchlem  31888  pnfinf  32599  1fldgenq  32682  rrhre  33299  erdszelem5  34484  wsuceq2  35092  taupilem1  36505  finxpreclem2  36574  sin2h  36781  cos2h  36782  tan2h  36783  poimirlem27  36818  poimirlem30  36821  broucube  36825  mblfinlem1  36828  heiborlem6  36987  lcmineqlem19  41218  2xp3dxp2ge1d  41328  onexomgt  42292  omabs2  42384  icccncfext  44901  dirkertrigeq  45115  zlmodzxzel  47119  dignn0flhalflem1  47388  2arymaptfo  47427  fv1prop  47472  fv2prop  47473  line2x  47527  onetansqsecsq  47893  cotsqcscsq  47894