Theorem mp3an13 1478

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  predeq2  6306  wrecseq2  8313  oeoalem  8582  mulrid  11206  addltmul  12480  fz01en  13580  fznatpl1  13606  expubnd  14214  bernneq  14265  bernneq2  14266  faclbnd4lem1  14329  hashfun  14474  bpoly2  16111  bpoly3  16112  fsumcube  16114  efi4p  16193  efival  16208  cos2tsin  16235  cos01bnd  16242  cos01gt0  16247  dvds0  16329  odd2np1  16399  opoe  16421  divalglem0  16451  gcdid  16585  pythagtriplem4  16879  ressid  17304  fvpr0o  17613  fvpr1o  17614  zringcyg  21588  lecldbas  23345  blssioo  24921  tgioo  24922  rerest  24930  xrrest  24934  zdis  24943  reconnlem2  24954  metdscn2  24984  negcncf  25050  iihalf2  25061  cncmet  25450  rrxmvallem  25532  rrxmval  25533  ovolunlem1a  25624  ismbf3d  25782  c1lip2  26126  pilem2  26581  pilem3  26582  sinperlem  26611  sincosq1sgn  26629  sincosq2sgn  26630  sinq12gt0  26638  cosq14gt0  26641  cosq14ge0  26642  coseq1  26656  sinord  26665  zetacvg  27145  1sgmprm  27329  ppiub  27334  chtublem  27341  chtub  27342  bcp1ctr  27409  bpos1lem  27412  bposlem2  27415  bposlem3  27416  bposlem4  27417  bposlem5  27418  bposlem6  27419  bposlem7  27420  bposlem9  27422  nnsge1  28502  pw2gt0divsd  28604  pw2ge0divsd  28605  pw2ltdivmulsd  28609  pw2ltmuldivs2d  28610  pw2ltdivmuls2d  28616  pw2cut  28619  bdayfinbndlem1  28626  axlowdim  29252  ipidsq  31003  ipasslem1  31124  ipasslem2  31125  ipasslem4  31127  ipasslem5  31128  ipasslem8  31130  ipasslem9  31131  ipasslem11  31133  pjoc1i  31724  h1de2bi  31847  h1de2ctlem  31848  spanunsni  31872  opsqrlem1  32433  opsqrlem6  32438  chrelati  32657  chrelat2i  32658  cvexchlem  32661  pnfinf  33444  1fldgenq  33586  rrhre  34356  erdszelem5  35620  wsuceq2  36239  taupilem1  37888  finxpreclem2  37959  sin2h  38184  cos2h  38185  tan2h  38186  poimirlem27  38221  poimirlem30  38224  broucube  38228  mblfinlem1  38231  heiborlem6  38390  lcmineqlem19  42739  onexomgt  43895  omabs2  43986  icccncfext  46528  dirkertrigeq  46742  pgnbgreunbgrlem4  48808  zlmodzxzel  49055  dignn0flhalflem1  49315  2arymaptfo  49354  fv1prop  49399  fv2prop  49400  line2x  49454  onetansqsecsq  50459  cotsqcscsq  50460