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  6257  wrecseq2  8255  oeoalem  8521  mulrid  11131  addltmul  12402  fz01en  13495  fznatpl1  13521  expubnd  14129  bernneq  14180  bernneq2  14181  faclbnd4lem1  14244  hashfun  14388  bpoly2  16011  bpoly3  16012  fsumcube  16014  efi4p  16093  efival  16108  cos2tsin  16135  cos01bnd  16142  cos01gt0  16147  dvds0  16229  odd2np1  16299  opoe  16321  divalglem0  16351  gcdid  16485  pythagtriplem4  16779  ressid  17203  fvpr0o  17512  fvpr1o  17513  zringcyg  21438  lecldbas  23172  blssioo  24748  tgioo  24749  rerest  24757  xrrest  24761  zdis  24770  reconnlem2  24781  metdscn2  24811  negcncf  24877  iihalf2  24888  cncmet  25277  rrxmvallem  25359  rrxmval  25360  ovolunlem1a  25451  ismbf3d  25609  c1lip2  25953  pilem2  26405  pilem3  26406  sinperlem  26432  sincosq1sgn  26450  sincosq2sgn  26451  sinq12gt0  26459  cosq14gt0  26462  cosq14ge0  26463  coseq1  26477  sinord  26486  zetacvg  26966  1sgmprm  27150  ppiub  27155  chtublem  27162  chtub  27163  bcp1ctr  27230  bpos1lem  27233  bposlem2  27236  bposlem3  27237  bposlem4  27238  bposlem5  27239  bposlem6  27240  bposlem7  27241  bposlem9  27243  nnsge1  28323  pw2gt0divsd  28425  pw2ge0divsd  28426  pw2ltdivmulsd  28430  pw2ltmuldivs2d  28431  pw2ltdivmuls2d  28437  pw2cut  28440  bdayfinbndlem1  28447  axlowdim  29018  ipidsq  30769  ipasslem1  30890  ipasslem2  30891  ipasslem4  30893  ipasslem5  30894  ipasslem8  30896  ipasslem9  30897  ipasslem11  30899  pjoc1i  31490  h1de2bi  31613  h1de2ctlem  31614  spanunsni  31638  opsqrlem1  32199  opsqrlem6  32204  chrelati  32423  chrelat2i  32424  cvexchlem  32427  pnfinf  33232  1fldgenq  33371  rrhre  34153  erdszelem5  35365  wsuceq2  35984  taupilem1  37623  finxpreclem2  37694  sin2h  37919  cos2h  37920  tan2h  37921  poimirlem27  37956  poimirlem30  37959  broucube  37963  mblfinlem1  37966  heiborlem6  38125  lcmineqlem19  42474  onexomgt  43657  omabs2  43748  icccncfext  46303  dirkertrigeq  46517  pgnbgreunbgrlem4  48583  zlmodzxzel  48819  dignn0flhalflem1  49079  2arymaptfo  49118  fv1prop  49163  fv2prop  49164  line2x  49218  onetansqsecsq  50224  cotsqcscsq  50225