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  6263  wrecseq2  8260  oeoalem  8526  mulrid  11134  addltmul  12381  fz01en  13472  fznatpl1  13498  expubnd  14105  bernneq  14156  bernneq2  14157  faclbnd4lem1  14220  hashfun  14364  bpoly2  15984  bpoly3  15985  fsumcube  15987  efi4p  16066  efival  16081  cos2tsin  16108  cos01bnd  16115  cos01gt0  16120  dvds0  16202  odd2np1  16272  opoe  16294  divalglem0  16324  gcdid  16458  pythagtriplem4  16751  ressid  17175  fvpr0o  17484  fvpr1o  17485  zringcyg  21428  lecldbas  23167  blssioo  24743  tgioo  24744  rerest  24752  xrrest  24756  zdis  24765  reconnlem2  24776  metdscn2  24806  negcncf  24875  negcncfOLD  24876  iihalf2  24888  cncmet  25282  rrxmvallem  25364  rrxmval  25365  ovolunlem1a  25457  ismbf3d  25615  c1lip2  25963  pilem2  26422  pilem3  26423  sinperlem  26449  sincosq1sgn  26467  sincosq2sgn  26468  sinq12gt0  26476  cosq14gt0  26479  cosq14ge0  26480  coseq1  26494  sinord  26503  zetacvg  26985  1sgmprm  27170  ppiub  27175  chtublem  27182  chtub  27183  bcp1ctr  27250  bpos1lem  27253  bposlem2  27256  bposlem3  27257  bposlem4  27258  bposlem5  27259  bposlem6  27260  bposlem7  27261  bposlem9  27263  nnsge1  28343  pw2gt0divsd  28445  pw2ge0divsd  28446  pw2ltdivmulsd  28450  pw2ltmuldivs2d  28451  pw2ltdivmuls2d  28457  pw2cut  28460  bdayfinbndlem1  28467  axlowdim  29038  ipidsq  30789  ipasslem1  30910  ipasslem2  30911  ipasslem4  30913  ipasslem5  30914  ipasslem8  30916  ipasslem9  30917  ipasslem11  30919  pjoc1i  31510  h1de2bi  31633  h1de2ctlem  31634  spanunsni  31658  opsqrlem1  32219  opsqrlem6  32224  chrelati  32443  chrelat2i  32444  cvexchlem  32447  pnfinf  33267  1fldgenq  33406  rrhre  34180  erdszelem5  35391  wsuceq2  36010  taupilem1  37528  finxpreclem2  37597  sin2h  37813  cos2h  37814  tan2h  37815  poimirlem27  37850  poimirlem30  37853  broucube  37857  mblfinlem1  37860  heiborlem6  38019  lcmineqlem19  42369  onexomgt  43550  omabs2  43641  icccncfext  46198  dirkertrigeq  46412  pgnbgreunbgrlem4  48432  zlmodzxzel  48668  dignn0flhalflem1  48928  2arymaptfo  48967  fv1prop  49012  fv2prop  49013  line2x  49067  onetansqsecsq  50073  cotsqcscsq  50074