Theorem mp3an13 1448

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  predeq2  6151  wrecseq2  7951  oeoalem  8222  mulid1  10639  addltmul  11874  eluzaddi  12272  fz01en  12936  fznatpl1  12962  expubnd  13542  bernneq  13591  bernneq2  13592  faclbnd4lem1  13654  hashfun  13799  bpoly2  15411  bpoly3  15412  fsumcube  15414  efi4p  15490  efival  15505  cos2tsin  15532  cos01bnd  15539  cos01gt0  15544  dvds0  15625  odd2np1  15690  opoe  15712  divalglem0  15744  gcdid  15875  pythagtriplem4  16156  ressid  16559  fvpr0o  16832  fvpr1o  16833  zringcyg  20638  lecldbas  21827  blssioo  23403  tgioo  23404  rerest  23412  xrrest  23415  zdis  23424  reconnlem2  23435  metdscn2  23465  negcncf  23526  iihalf2  23537  cncmet  23925  rrxmvallem  24007  rrxmval  24008  ovolunlem1a  24097  ismbf3d  24255  c1lip2  24595  pilem2  25040  pilem3  25041  sinperlem  25066  sincosq1sgn  25084  sincosq2sgn  25085  sinq12gt0  25093  cosq14gt0  25096  cosq14ge0  25097  coseq1  25110  sinord  25118  zetacvg  25592  1sgmprm  25775  ppiub  25780  chtublem  25787  chtub  25788  bcp1ctr  25855  bpos1lem  25858  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  bposlem9  25868  axlowdim  26747  ipidsq  28487  ipasslem1  28608  ipasslem2  28609  ipasslem4  28611  ipasslem5  28612  ipasslem8  28614  ipasslem9  28615  ipasslem11  28617  pjoc1i  29208  h1de2bi  29331  h1de2ctlem  29332  spanunsni  29356  opsqrlem1  29917  opsqrlem6  29922  chrelati  30141  chrelat2i  30142  cvexchlem  30145  pnfinf  30812  rrhre  31262  erdszelem5  32442  wsuceq2  33103  taupilem1  34605  finxpreclem2  34674  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem27  34934  poimirlem30  34937  broucube  34941  mblfinlem1  34944  heiborlem6  35109  2xp3dxp2ge1d  39117  icccncfext  42190  dirkertrigeq  42406  zlmodzxzel  44423  dignn0flhalflem1  44695  fv1prop  44706  fv2prop  44707  line2x  44761  onetansqsecsq  44880  cotsqcscsq  44881