Theorem mp3an23 1481

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1478	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 703	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  sbciegf  3781  predeq1  6304  wrecseq1  8310  ac6sfi  9242  unfilem1  9263  fiint  9284  ordtypelem2  9479  infxpenc2  10013  dju0en  10166  cfsmolem  10260  axdc4lem  10445  1nqenq  10953  mul02lem1  11392  muleqadd  11864  2halves  12468  halfcl  12476  rehalfcl  12477  half0  12478  halfpos2  12479  halfnneg2  12481  halfaddsub  12483  nneo  12686  zeo  12688  peano5uzi  12691  fztp  13615  uzrdgxfr  14010  bcn2  14362  bcpasc  14364  hashxplem  14477  hashfun  14481  swrds2  14984  repsw2  14994  repsw3  14995  imre  15166  reim  15167  crim  15173  addcj  15206  imval2  15209  cnpart  15298  01sqrexlem7  15306  absmax  15388  binomfallfaclem2  16100  bpoly2  16117  bpoly3  16118  fsumcube  16120  efgt0  16165  sinf  16186  efi4p  16199  resin4p  16200  recos4p  16201  sinneg  16208  efival  16214  cosadd  16227  sinmul  16234  sinbnd  16242  cosbnd  16243  ef01bndlem  16246  sin01bnd  16247  cos01bnd  16248  sin01gt0  16252  cos01gt0  16253  sin02gt0  16254  rpnnen2lem11  16286  rpnnen2lem12  16287  odd2np1lem  16404  odd2np1  16405  pythagtriplem12  16892  pythagtriplem14  16894  pythagtriplem15  16895  pythagtriplem16  16896  pythagtriplem17  16897  pockthi  16973  prmreclem5  16986  prmreclem6  16987  prmlem0  17171  prdsplusg  17517  prdsmulr  17518  prdsvsca  17519  isghm  19292  odinf  19639  ogrpaddlt  20214  ofldlt1  20989  lbsexg  21299  ofldchr  21737  psgnghm2  21742  mopnex  24687  tngnm  24819  tngngp2  24820  tngngpd  24821  tngngp  24822  addccncf  25087  sub1cncf  25089  sub2cncf  25090  iihalf1  25101  iihalf2  25103  pjthlem1  25607  ovolunlem1a  25666  ovolunlem1  25667  opnmbllem  25771  vitalilem4  25781  iblcnlem1  25958  itgcnlem  25960  dvmptre  26139  dvmptim  26140  dvlipcn  26164  mdegldg  26234  aaliou3lem3  26518  aaliou3lem8  26519  sincosq1lem  26673  sincosq2sgn  26675  sincosq3sgn  26676  sincosq4sgn  26677  sinq12gt0  26683  abssinper  26697  coskpi  26699  sineq0  26700  coseq1  26701  efeq1  26704  resinf1o  26712  efif1olem2  26719  efif1olem4  26721  logneg2  26791  cxpsqrtlem  26878  cxpsqrt  26879  logsqrt  26880  1cubr  27018  leibpilem2  27117  basellem3  27258  ppiub  27379  chtublem  27386  chtub  27387  bcmax  27453  bcp1ctr  27454  bposlem2  27460  bposlem6  27464  bposlem9  27467  logdivsum  27708  elno  27821  mulscl  28338  4ipval2  31071  ipidsq  31073  dipcl  31075  dipcj  31077  ipasslem11  31203  hvmul0  31387  pjhthlem1  31754  h1de2bi  31917  spanunsni  31942  adjeu  32252  nmopge0  32274  nmfnge0  32290  opsqrlem6  32508  mdsl1i  32684  mdsl2bi  32686  mdexchi  32698  superpos  32717  atabsi  32764  dmdbr5ati  32785  cdj3lem1  32797  fpwrelmapffslem  33088  dp2cl  33210  dpfrac1  33222  cshw1s2  33289  oddpwdc  34753  eulerpartgbij  34771  subfacp1lem2a  35680  subfacp1lem5  35684  subfacp1lem6  35685  subfaclim  35688  sinccvglem  36172  dfon2lem3  36283  dfon2lem7  36287  wsuceq1  36313  clsun  36867  vtoclefex  38008  finxpreclem5  38069  sin2h  38289  cos2h  38290  tan2h  38291  poimirlem22  38321  poimirlem31  38330  opnmbllem0  38335  mblfinlem3  38338  itg2addnclem3  38352  ftc1cnnclem  38370  ftc1anclem6  38377  ftc2nc  38381  dvasin  38383  fdc  38424  constcncf  38441  heiborlem7  38496  atlatmstc  40121  lcmineqlem10  42833  lcmineqlem12  42835  facp2  42938  3rdpwhole  43081  sn-00idlem1  43187  0prjspnlem  43383  sn-isghm  43433  diophren  43568  oaabsb  44049  dftrcl3  44474  dfrtrcl3  44487  cotrclrcl  44496  lhe4.4ex1a  45067  dirkerper  46838  sinnpoly  47656  zlmodzxznm  49305  sinh-conventional  50545