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  6251  wrecseq2  8246  oeoalem  8511  mulrid  11110  addltmul  12357  eluzaddiOLD  12764  fz01en  13452  fznatpl1  13478  expubnd  14085  bernneq  14136  bernneq2  14137  faclbnd4lem1  14200  hashfun  14344  bpoly2  15964  bpoly3  15965  fsumcube  15967  efi4p  16046  efival  16061  cos2tsin  16088  cos01bnd  16095  cos01gt0  16100  dvds0  16182  odd2np1  16252  opoe  16274  divalglem0  16304  gcdid  16438  pythagtriplem4  16731  ressid  17155  fvpr0o  17463  fvpr1o  17464  zringcyg  21406  lecldbas  23134  blssioo  24710  tgioo  24711  rerest  24719  xrrest  24723  zdis  24732  reconnlem2  24743  metdscn2  24773  negcncf  24842  negcncfOLD  24843  iihalf2  24855  cncmet  25249  rrxmvallem  25331  rrxmval  25332  ovolunlem1a  25424  ismbf3d  25582  c1lip2  25930  pilem2  26389  pilem3  26390  sinperlem  26416  sincosq1sgn  26434  sincosq2sgn  26435  sinq12gt0  26443  cosq14gt0  26446  cosq14ge0  26447  coseq1  26461  sinord  26470  zetacvg  26952  1sgmprm  27137  ppiub  27142  chtublem  27149  chtub  27150  bcp1ctr  27217  bpos1lem  27220  bposlem2  27223  bposlem3  27224  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem7  27228  bposlem9  27230  nnsge1  28271  pw2gt0divsd  28368  pw2ge0divsd  28369  pw2sltdivmuld  28373  pw2sltmuldiv2d  28374  pw2cut  28380  zs12bday  28394  axlowdim  28939  ipidsq  30690  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem5  30815  ipasslem8  30817  ipasslem9  30818  ipasslem11  30820  pjoc1i  31411  h1de2bi  31534  h1de2ctlem  31535  spanunsni  31559  opsqrlem1  32120  opsqrlem6  32125  chrelati  32344  chrelat2i  32345  cvexchlem  32348  pnfinf  33152  1fldgenq  33288  rrhre  34034  erdszelem5  35239  wsuceq2  35858  taupilem1  37365  finxpreclem2  37434  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem27  37686  poimirlem30  37689  broucube  37693  mblfinlem1  37696  heiborlem6  37855  lcmineqlem19  42139  onexomgt  43333  omabs2  43424  icccncfext  45984  dirkertrigeq  46198  pgnbgreunbgrlem4  48218  zlmodzxzel  48454  dignn0flhalflem1  48715  2arymaptfo  48754  fv1prop  48799  fv2prop  48800  line2x  48854  onetansqsecsq  49861  cotsqcscsq  49862