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  6266  wrecseq2  8263  oeoalem  8529  mulrid  11139  addltmul  12410  fz01en  13503  fznatpl1  13529  expubnd  14137  bernneq  14188  bernneq2  14189  faclbnd4lem1  14252  hashfun  14396  bpoly2  16019  bpoly3  16020  fsumcube  16022  efi4p  16101  efival  16116  cos2tsin  16143  cos01bnd  16150  cos01gt0  16155  dvds0  16237  odd2np1  16307  opoe  16329  divalglem0  16359  gcdid  16493  pythagtriplem4  16787  ressid  17211  fvpr0o  17520  fvpr1o  17521  zringcyg  21465  lecldbas  23200  blssioo  24776  tgioo  24777  rerest  24785  xrrest  24789  zdis  24798  reconnlem2  24809  metdscn2  24839  negcncf  24905  iihalf2  24916  cncmet  25305  rrxmvallem  25387  rrxmval  25388  ovolunlem1a  25479  ismbf3d  25637  c1lip2  25981  pilem2  26436  pilem3  26437  sinperlem  26463  sincosq1sgn  26481  sincosq2sgn  26482  sinq12gt0  26490  cosq14gt0  26493  cosq14ge0  26494  coseq1  26508  sinord  26517  zetacvg  26998  1sgmprm  27182  ppiub  27187  chtublem  27194  chtub  27195  bcp1ctr  27262  bpos1lem  27265  bposlem2  27268  bposlem3  27269  bposlem4  27270  bposlem5  27271  bposlem6  27272  bposlem7  27273  bposlem9  27275  nnsge1  28355  pw2gt0divsd  28457  pw2ge0divsd  28458  pw2ltdivmulsd  28462  pw2ltmuldivs2d  28463  pw2ltdivmuls2d  28469  pw2cut  28472  bdayfinbndlem1  28479  axlowdim  29050  ipidsq  30802  ipasslem1  30923  ipasslem2  30924  ipasslem4  30926  ipasslem5  30927  ipasslem8  30929  ipasslem9  30930  ipasslem11  30932  pjoc1i  31523  h1de2bi  31646  h1de2ctlem  31647  spanunsni  31671  opsqrlem1  32232  opsqrlem6  32237  chrelati  32456  chrelat2i  32457  cvexchlem  32460  pnfinf  33265  1fldgenq  33404  rrhre  34187  erdszelem5  35399  wsuceq2  36018  taupilem1  37657  finxpreclem2  37728  sin2h  37953  cos2h  37954  tan2h  37955  poimirlem27  37990  poimirlem30  37993  broucube  37997  mblfinlem1  38000  heiborlem6  38159  lcmineqlem19  42508  onexomgt  43695  omabs2  43786  icccncfext  46341  dirkertrigeq  46555  pgnbgreunbgrlem4  48615  zlmodzxzel  48851  dignn0flhalflem1  49111  2arymaptfo  49150  fv1prop  49195  fv2prop  49196  line2x  49250  onetansqsecsq  50256  cotsqcscsq  50257