Theorem mp3an23 1482

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 1479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 704	1 ⊢ (𝜑 → 𝜃)

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

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 402  df-3an 1105

This theorem is used by:  sbciegf  3777  predeq1  6296  wrecseq1  8312  ac6sfi  9254  unfilem1  9275  fiint  9296  ordtypelem2  9491  infxpenc2  10058  dju0en  10211  cfsmolem  10305  axdc4lem  10490  1nqenq  11004  mul02lem1  11443  muleqadd  11915  2halves  12519  halfcl  12527  rehalfcl  12528  half0  12529  halfpos2  12530  halfnneg2  12532  halfaddsub  12534  nneo  12738  zeo  12740  peano5uzi  12743  fztp  13668  uzrdgxfr  14064  bcn2  14416  bcpasc  14418  hashxplem  14531  hashfun  14535  swrds2  15044  repsw2  15056  repsw3  15057  imre  15228  reim  15229  crim  15235  addcj  15268  imval2  15271  cnpart  15360  01sqrexlem7  15368  absmax  15450  binomfallfaclem2  16159  bpoly2  16176  bpoly3  16177  fsumcube  16179  efgt0  16224  sinf  16245  efi4p  16258  resin4p  16259  recos4p  16260  sinneg  16267  efival  16273  cosadd  16286  sinmul  16293  sinbnd  16301  cosbnd  16302  ef01bndlem  16305  sin01bnd  16306  cos01bnd  16307  sin01gt0  16311  cos01gt0  16312  sin02gt0  16313  rpnnen2lem11  16345  rpnnen2lem12  16346  odd2np1lem  16463  odd2np1  16464  pythagtriplem12  16951  pythagtriplem14  16953  pythagtriplem15  16954  pythagtriplem16  16955  pythagtriplem17  16956  pockthi  17032  prmreclem5  17045  prmreclem6  17046  prmlem0  17230  prdsplusg  17576  prdsmulr  17577  prdsvsca  17578  isghm  19377  odinf  19724  ogrpaddlt  20299  ofldlt1  21079  lbsexg  21389  ofldchr  21829  psgnghm2  21834  mopnex  24785  tngnm  24917  tngngp2  24918  tngngpd  24919  tngngp  24920  addccncf  25185  sub1cncf  25187  sub2cncf  25188  iihalf1  25199  iihalf2  25201  pjthlem1  25705  ovolunlem1a  25764  ovolunlem1  25765  opnmbllem  25869  vitalilem4  25879  iblcnlem1  26055  itgcnlem  26057  dvmptre  26236  dvmptim  26237  dvlipcn  26261  mdegldg  26331  aaliou3lem3  26620  aaliou3lem8  26621  sincosq1lem  26775  sincosq2sgn  26777  sincosq3sgn  26778  sincosq4sgn  26779  sinq12gt0  26785  abssinper  26798  coskpi  26800  sineq0  26801  coseq1  26802  efeq1  26805  resinf1o  26813  efif1olem2  26820  efif1olem4  26822  logneg2  26892  cxpsqrtlem  26979  cxpsqrt  26980  logsqrt  26981  1cubr  27119  leibpilem2  27218  basellem3  27359  ppiub  27480  chtublem  27487  chtub  27488  bcmax  27554  bcp1ctr  27555  bposlem2  27561  bposlem6  27565  bposlem9  27568  logdivsum  27809  elno  27922  mulscl  28439  4ipval2  31229  ipidsq  31231  dipcl  31233  dipcj  31235  ipasslem11  31361  hvmul0  31545  pjhthlem1  31912  h1de2bi  32075  spanunsni  32100  adjeu  32410  nmopge0  32432  nmfnge0  32448  opsqrlem6  32666  mdsl1i  32842  mdsl2bi  32844  mdexchi  32856  superpos  32875  atabsi  32922  dmdbr5ati  32943  cdj3lem1  32955  fpwrelmapffslem  33243  dp2cl  33365  dpfrac1  33377  cshw1s2  33440  oddpwdc  34906  eulerpartgbij  34924  subfacp1lem2a  35860  subfacp1lem5  35864  subfacp1lem6  35865  subfaclim  35868  sinccvglem  36352  dfon2lem3  36463  dfon2lem7  36467  wsuceq1  36493  clsun  37032  vtoclefex  38171  finxpreclem5  38232  sin2h  38447  cos2h  38448  tan2h  38449  poimirlem22  38474  poimirlem31  38483  opnmbllem0  38488  mblfinlem3  38491  itg2addnclem3  38505  ftc1cnnclem  38523  ftc1anclem6  38530  ftc2nc  38534  dvasin  38536  fdc  38593  constcncf  38610  heiborlem7  38665  atlatmstc  40290  lcmineqlem10  43002  lcmineqlem12  43004  facp2  43107  3rdpwhole  43265  sn-00idlem1  43371  0prjspnlem  43567  sn-isghm  43617  diophren  43752  oaabsb  44233  dftrcl3  44658  dfrtrcl3  44671  cotrclrcl  44680  lhe4.4ex1a  45251  dirkerper  47022  sinnpoly  47857  zlmodzxznm  49525  sinh-conventional  50748