Theorem mp3an13 1461

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  predeq2  6259  wrecseq2  8260  oeoalem  8526  mulrid  11137  addltmul  12408  fz01en  13501  fznatpl1  13527  expubnd  14135  bernneq  14186  bernneq2  14187  faclbnd4lem1  14250  hashfun  14394  bpoly2  16017  bpoly3  16018  fsumcube  16020  efi4p  16099  efival  16114  cos2tsin  16141  cos01bnd  16148  cos01gt0  16153  dvds0  16235  odd2np1  16305  opoe  16327  divalglem0  16357  gcdid  16491  pythagtriplem4  16785  ressid  17209  fvpr0o  17518  fvpr1o  17519  zringcyg  21448  lecldbas  23206  blssioo  24782  tgioo  24783  rerest  24791  xrrest  24795  zdis  24804  reconnlem2  24815  metdscn2  24845  negcncf  24911  iihalf2  24922  cncmet  25311  rrxmvallem  25393  rrxmval  25394  ovolunlem1a  25485  ismbf3d  25643  c1lip2  25987  pilem2  26439  pilem3  26440  sinperlem  26466  sincosq1sgn  26484  sincosq2sgn  26485  sinq12gt0  26493  cosq14gt0  26496  cosq14ge0  26497  coseq1  26511  sinord  26520  zetacvg  27000  1sgmprm  27184  ppiub  27189  chtublem  27196  chtub  27197  bcp1ctr  27264  bpos1lem  27267  bposlem2  27270  bposlem3  27271  bposlem4  27272  bposlem5  27273  bposlem6  27274  bposlem7  27275  bposlem9  27277  nnsge1  28357  pw2gt0divsd  28459  pw2ge0divsd  28460  pw2ltdivmulsd  28464  pw2ltmuldivs2d  28465  pw2ltdivmuls2d  28471  pw2cut  28474  bdayfinbndlem1  28481  axlowdim  29052  ipidsq  30803  ipasslem1  30924  ipasslem2  30925  ipasslem4  30927  ipasslem5  30928  ipasslem8  30930  ipasslem9  30931  ipasslem11  30933  pjoc1i  31524  h1de2bi  31647  h1de2ctlem  31648  spanunsni  31672  opsqrlem1  32233  opsqrlem6  32238  chrelati  32457  chrelat2i  32458  cvexchlem  32461  pnfinf  33268  1fldgenq  33410  rrhre  34217  erdszelem5  35438  wsuceq2  36057  taupilem1  37696  finxpreclem2  37767  sin2h  37992  cos2h  37993  tan2h  37994  poimirlem27  38029  poimirlem30  38032  broucube  38036  mblfinlem1  38039  heiborlem6  38198  lcmineqlem19  42547  onexomgt  43701  omabs2  43792  icccncfext  46344  dirkertrigeq  46558  pgnbgreunbgrlem4  48624  zlmodzxzel  48860  dignn0flhalflem1  49120  2arymaptfo  49159  fv1prop  49204  fv2prop  49205  line2x  49259  onetansqsecsq  50265  cotsqcscsq  50266