Theorem mp3an13 1454

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  predeq2  6266  wrecseq2  8273  oeoalem  8538  mulrid  11151  addltmul  12397  eluzaddiOLD  12804  fz01en  13492  fznatpl1  13518  expubnd  14122  bernneq  14173  bernneq2  14174  faclbnd4lem1  14237  hashfun  14381  bpoly2  16001  bpoly3  16002  fsumcube  16004  efi4p  16083  efival  16098  cos2tsin  16125  cos01bnd  16132  cos01gt0  16137  dvds0  16219  odd2np1  16289  opoe  16311  divalglem0  16341  gcdid  16475  pythagtriplem4  16768  ressid  17192  fvpr0o  17500  fvpr1o  17501  zringcyg  21413  lecldbas  23141  blssioo  24718  tgioo  24719  rerest  24727  xrrest  24731  zdis  24740  reconnlem2  24751  metdscn2  24781  negcncf  24850  negcncfOLD  24851  iihalf2  24863  cncmet  25257  rrxmvallem  25339  rrxmval  25340  ovolunlem1a  25432  ismbf3d  25590  c1lip2  25938  pilem2  26397  pilem3  26398  sinperlem  26424  sincosq1sgn  26442  sincosq2sgn  26443  sinq12gt0  26451  cosq14gt0  26454  cosq14ge0  26455  coseq1  26469  sinord  26478  zetacvg  26960  1sgmprm  27145  ppiub  27150  chtublem  27157  chtub  27158  bcp1ctr  27225  bpos1lem  27228  bposlem2  27231  bposlem3  27232  bposlem4  27233  bposlem5  27234  bposlem6  27235  bposlem7  27236  bposlem9  27238  nnsge1  28277  pw2gt0divsd  28374  pw2ge0divsd  28375  pw2sltdivmuld  28379  pw2sltmuldiv2d  28380  pw2cut  28385  zs12bday  28398  axlowdim  28943  ipidsq  30691  ipasslem1  30812  ipasslem2  30813  ipasslem4  30815  ipasslem5  30816  ipasslem8  30818  ipasslem9  30819  ipasslem11  30821  pjoc1i  31412  h1de2bi  31535  h1de2ctlem  31536  spanunsni  31560  opsqrlem1  32121  opsqrlem6  32126  chrelati  32345  chrelat2i  32346  cvexchlem  32349  pnfinf  33154  1fldgenq  33290  rrhre  34006  erdszelem5  35177  wsuceq2  35799  taupilem1  37304  finxpreclem2  37373  sin2h  37599  cos2h  37600  tan2h  37601  poimirlem27  37636  poimirlem30  37639  broucube  37643  mblfinlem1  37646  heiborlem6  37805  lcmineqlem19  42030  onexomgt  43225  omabs2  43316  icccncfext  45880  dirkertrigeq  46094  pgnbgreunbgrlem4  48104  zlmodzxzel  48338  dignn0flhalflem1  48599  2arymaptfo  48638  fv1prop  48683  fv2prop  48684  line2x  48738  onetansqsecsq  49745  cotsqcscsq  49746