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  6272  wrecseq2  8270  oeoalem  8536  mulrid  11144  addltmul  12391  fz01en  13482  fznatpl1  13508  expubnd  14115  bernneq  14166  bernneq2  14167  faclbnd4lem1  14230  hashfun  14374  bpoly2  15994  bpoly3  15995  fsumcube  15997  efi4p  16076  efival  16091  cos2tsin  16118  cos01bnd  16125  cos01gt0  16130  dvds0  16212  odd2np1  16282  opoe  16304  divalglem0  16334  gcdid  16468  pythagtriplem4  16761  ressid  17185  fvpr0o  17494  fvpr1o  17495  zringcyg  21441  lecldbas  23180  blssioo  24756  tgioo  24757  rerest  24765  xrrest  24769  zdis  24778  reconnlem2  24789  metdscn2  24819  negcncf  24888  negcncfOLD  24889  iihalf2  24901  cncmet  25295  rrxmvallem  25377  rrxmval  25378  ovolunlem1a  25470  ismbf3d  25628  c1lip2  25976  pilem2  26435  pilem3  26436  sinperlem  26462  sincosq1sgn  26480  sincosq2sgn  26481  sinq12gt0  26489  cosq14gt0  26492  cosq14ge0  26493  coseq1  26507  sinord  26516  zetacvg  26998  1sgmprm  27183  ppiub  27188  chtublem  27195  chtub  27196  bcp1ctr  27263  bpos1lem  27266  bposlem2  27269  bposlem3  27270  bposlem4  27271  bposlem5  27272  bposlem6  27273  bposlem7  27274  bposlem9  27276  nnsge1  28356  pw2gt0divsd  28458  pw2ge0divsd  28459  pw2ltdivmulsd  28463  pw2ltmuldivs2d  28464  pw2ltdivmuls2d  28470  pw2cut  28473  bdayfinbndlem1  28480  axlowdim  29052  ipidsq  30804  ipasslem1  30925  ipasslem2  30926  ipasslem4  30928  ipasslem5  30929  ipasslem8  30931  ipasslem9  30932  ipasslem11  30934  pjoc1i  31525  h1de2bi  31648  h1de2ctlem  31649  spanunsni  31673  opsqrlem1  32234  opsqrlem6  32239  chrelati  32458  chrelat2i  32459  cvexchlem  32462  pnfinf  33283  1fldgenq  33422  rrhre  34205  erdszelem5  35417  wsuceq2  36036  taupilem1  37603  finxpreclem2  37672  sin2h  37890  cos2h  37891  tan2h  37892  poimirlem27  37927  poimirlem30  37930  broucube  37934  mblfinlem1  37937  heiborlem6  38096  lcmineqlem19  42446  onexomgt  43627  omabs2  43718  icccncfext  46274  dirkertrigeq  46488  pgnbgreunbgrlem4  48508  zlmodzxzel  48744  dignn0flhalflem1  49004  2arymaptfo  49043  fv1prop  49088  fv2prop  49089  line2x  49143  onetansqsecsq  50149  cotsqcscsq  50150