Theorem mp3an13 1454

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 1452	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 690	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  predeq2  6293  wrecseq2  8316  oeoalem  8606  mulrid  11231  addltmul  12475  eluzaddiOLD  12882  fz01en  13567  fznatpl1  13593  expubnd  14194  bernneq  14245  bernneq2  14246  faclbnd4lem1  14309  hashfun  14453  bpoly2  16071  bpoly3  16072  fsumcube  16074  efi4p  16153  efival  16168  cos2tsin  16195  cos01bnd  16202  cos01gt0  16207  dvds0  16289  odd2np1  16358  opoe  16380  divalglem0  16410  gcdid  16544  pythagtriplem4  16837  ressid  17263  fvpr0o  17571  fvpr1o  17572  zringcyg  21428  lecldbas  23155  blssioo  24732  tgioo  24733  rerest  24741  xrrest  24745  zdis  24754  reconnlem2  24765  metdscn2  24795  negcncf  24864  negcncfOLD  24865  iihalf2  24877  cncmet  25272  rrxmvallem  25354  rrxmval  25355  ovolunlem1a  25447  ismbf3d  25605  c1lip2  25953  pilem2  26412  pilem3  26413  sinperlem  26439  sincosq1sgn  26457  sincosq2sgn  26458  sinq12gt0  26466  cosq14gt0  26469  cosq14ge0  26470  coseq1  26484  sinord  26493  zetacvg  26975  1sgmprm  27160  ppiub  27165  chtublem  27172  chtub  27173  bcp1ctr  27240  bpos1lem  27243  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem7  27251  bposlem9  27253  nnsge1  28263  cutpw2  28334  pw2bday  28335  pw2cut  28337  zs12bday  28341  axlowdim  28886  ipidsq  30637  ipasslem1  30758  ipasslem2  30759  ipasslem4  30761  ipasslem5  30762  ipasslem8  30764  ipasslem9  30765  ipasslem11  30767  pjoc1i  31358  h1de2bi  31481  h1de2ctlem  31482  spanunsni  31506  opsqrlem1  32067  opsqrlem6  32072  chrelati  32291  chrelat2i  32292  cvexchlem  32295  pnfinf  33127  1fldgenq  33262  rrhre  33998  erdszelem5  35163  wsuceq2  35780  taupilem1  37285  finxpreclem2  37354  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem27  37617  poimirlem30  37620  broucube  37624  mblfinlem1  37627  heiborlem6  37786  lcmineqlem19  42006  2xp3dxp2ge1d  42200  onexomgt  43212  omabs2  43303  icccncfext  45864  dirkertrigeq  46078  zlmodzxzel  48278  dignn0flhalflem1  48543  2arymaptfo  48582  fv1prop  48627  fv2prop  48628  line2x  48682  onetansqsecsq  49573  cotsqcscsq  49574