Theorem mp3an13 1449

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  predeq2  6119  wrecseq2  7934  oeoalem  8205  mulid1  10628  addltmul  11861  eluzaddi  12259  fz01en  12930  fznatpl1  12956  expubnd  13537  bernneq  13586  bernneq2  13587  faclbnd4lem1  13649  hashfun  13794  bpoly2  15403  bpoly3  15404  fsumcube  15406  efi4p  15482  efival  15497  cos2tsin  15524  cos01bnd  15531  cos01gt0  15536  dvds0  15617  odd2np1  15682  opoe  15704  divalglem0  15734  gcdid  15865  pythagtriplem4  16146  ressid  16551  fvpr0o  16824  fvpr1o  16825  zringcyg  20184  lecldbas  21824  blssioo  23400  tgioo  23401  rerest  23409  xrrest  23412  zdis  23421  reconnlem2  23432  metdscn2  23462  negcncf  23527  iihalf2  23538  cncmet  23926  rrxmvallem  24008  rrxmval  24009  ovolunlem1a  24100  ismbf3d  24258  c1lip2  24601  pilem2  25047  pilem3  25048  sinperlem  25073  sincosq1sgn  25091  sincosq2sgn  25092  sinq12gt0  25100  cosq14gt0  25103  cosq14ge0  25104  coseq1  25117  sinord  25126  zetacvg  25600  1sgmprm  25783  ppiub  25788  chtublem  25795  chtub  25796  bcp1ctr  25863  bpos1lem  25866  bposlem2  25869  bposlem3  25870  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem7  25874  bposlem9  25876  axlowdim  26755  ipidsq  28493  ipasslem1  28614  ipasslem2  28615  ipasslem4  28617  ipasslem5  28618  ipasslem8  28620  ipasslem9  28621  ipasslem11  28623  pjoc1i  29214  h1de2bi  29337  h1de2ctlem  29338  spanunsni  29362  opsqrlem1  29923  opsqrlem6  29928  chrelati  30147  chrelat2i  30148  cvexchlem  30151  pnfinf  30862  rrhre  31372  erdszelem5  32555  wsuceq2  33216  taupilem1  34735  finxpreclem2  34807  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem27  35084  poimirlem30  35087  broucube  35091  mblfinlem1  35094  heiborlem6  35254  lcmineqlem19  39335  2xp3dxp2ge1d  39387  icccncfext  42529  dirkertrigeq  42743  zlmodzxzel  44757  dignn0flhalflem1  45029  2arymaptfo  45068  fv1prop  45113  fv2prop  45114  line2x  45168  onetansqsecsq  45287  cotsqcscsq  45288