Theorem mp3an13 1455

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 1453	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 691	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:  predeq2  6268  wrecseq2  8266  oeoalem  8532  mulrid  11142  addltmul  12413  fz01en  13506  fznatpl1  13532  expubnd  14140  bernneq  14191  bernneq2  14192  faclbnd4lem1  14255  hashfun  14399  bpoly2  16022  bpoly3  16023  fsumcube  16025  efi4p  16104  efival  16119  cos2tsin  16146  cos01bnd  16153  cos01gt0  16158  dvds0  16240  odd2np1  16310  opoe  16332  divalglem0  16362  gcdid  16496  pythagtriplem4  16790  ressid  17214  fvpr0o  17523  fvpr1o  17524  zringcyg  21449  lecldbas  23184  blssioo  24760  tgioo  24761  rerest  24769  xrrest  24773  zdis  24782  reconnlem2  24793  metdscn2  24823  negcncf  24889  iihalf2  24900  cncmet  25289  rrxmvallem  25371  rrxmval  25372  ovolunlem1a  25463  ismbf3d  25621  c1lip2  25965  pilem2  26417  pilem3  26418  sinperlem  26444  sincosq1sgn  26462  sincosq2sgn  26463  sinq12gt0  26471  cosq14gt0  26474  cosq14ge0  26475  coseq1  26489  sinord  26498  zetacvg  26978  1sgmprm  27162  ppiub  27167  chtublem  27174  chtub  27175  bcp1ctr  27242  bpos1lem  27245  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  bposlem9  27255  nnsge1  28335  pw2gt0divsd  28437  pw2ge0divsd  28438  pw2ltdivmulsd  28442  pw2ltmuldivs2d  28443  pw2ltdivmuls2d  28449  pw2cut  28452  bdayfinbndlem1  28459  axlowdim  29030  ipidsq  30781  ipasslem1  30902  ipasslem2  30903  ipasslem4  30905  ipasslem5  30906  ipasslem8  30908  ipasslem9  30909  ipasslem11  30911  pjoc1i  31502  h1de2bi  31625  h1de2ctlem  31626  spanunsni  31650  opsqrlem1  32211  opsqrlem6  32216  chrelati  32435  chrelat2i  32436  cvexchlem  32439  pnfinf  33244  1fldgenq  33383  rrhre  34165  erdszelem5  35377  wsuceq2  35996  taupilem1  37635  finxpreclem2  37706  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem27  37968  poimirlem30  37971  broucube  37975  mblfinlem1  37978  heiborlem6  38137  lcmineqlem19  42486  onexomgt  43669  omabs2  43760  icccncfext  46315  dirkertrigeq  46529  pgnbgreunbgrlem4  48595  zlmodzxzel  48831  dignn0flhalflem1  49091  2arymaptfo  49130  fv1prop  49175  fv2prop  49176  line2x  49230  onetansqsecsq  50236  cotsqcscsq  50237