Theorem mp3an23 1455

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 1452	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 691	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:  sbciegf  3781  predeq1  6251  wrecseq1  8248  ac6sfi  9173  unfilem1  9194  fiint  9216  ordtypelem2  9411  infxpenc2  9916  dju0en  10070  cfsmolem  10164  axdc4lem  10349  1nqenq  10856  mul02lem1  11292  muleqadd  11764  2halves  12342  halfcl  12350  rehalfcl  12351  half0  12352  halfpos2  12353  halfnneg2  12355  halfaddsub  12357  nneo  12560  zeo  12562  peano5uzi  12565  fztp  13483  uzrdgxfr  13874  bcn2  14226  bcpasc  14228  hashxplem  14340  hashfun  14344  swrds2  14847  repsw2  14857  repsw3  14858  imre  15015  reim  15016  crim  15022  addcj  15055  imval2  15058  cnpart  15147  01sqrexlem7  15155  absmax  15237  binomfallfaclem2  15947  bpoly2  15964  bpoly3  15965  fsumcube  15967  efgt0  16012  sinf  16033  efi4p  16046  resin4p  16047  recos4p  16048  sinneg  16055  efival  16061  cosadd  16074  sinmul  16081  sinbnd  16089  cosbnd  16090  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  rpnnen2lem11  16133  rpnnen2lem12  16134  odd2np1lem  16251  odd2np1  16252  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem15  16741  pythagtriplem16  16742  pythagtriplem17  16743  pockthi  16819  prmreclem5  16832  prmreclem6  16833  prmlem0  17017  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  isghm  19094  odinf  19442  ogrpaddlt  20017  ofldlt1  20760  lbsexg  21071  ofldchr  21483  psgnghm2  21488  mopnex  24405  tngnm  24537  tngngp2  24538  tngngpd  24539  tngngp  24540  addccncf  24808  sub1cncf  24810  sub2cncf  24811  iihalf1  24823  iihalf2  24826  pjthlem1  25335  ovolunlem1a  25395  ovolunlem1  25396  opnmbllem  25500  vitalilem4  25510  iblcnlem1  25687  itgcnlem  25689  dvmptre  25871  dvmptim  25872  dvlipcn  25897  mdegldg  25969  aaliou3lem3  26250  aaliou3lem8  26251  sincosq1lem  26404  sincosq2sgn  26406  sincosq3sgn  26407  sincosq4sgn  26408  sinq12gt0  26414  abssinper  26428  coskpi  26430  sineq0  26431  coseq1  26432  efeq1  26435  resinf1o  26443  efif1olem2  26450  efif1olem4  26452  logneg2  26522  cxpsqrtlem  26609  cxpsqrt  26610  logsqrt  26611  1cubr  26750  leibpilem2  26849  basellem3  26991  ppiub  27113  chtublem  27120  chtub  27121  bcmax  27187  bcp1ctr  27188  bposlem2  27194  bposlem6  27198  bposlem9  27201  logdivsum  27442  elno  27555  mulscl  28044  4ipval2  30656  ipidsq  30658  dipcl  30660  dipcj  30662  ipasslem11  30788  hvmul0  30972  pjhthlem1  31339  h1de2bi  31502  spanunsni  31527  adjeu  31837  nmopge0  31859  nmfnge0  31875  opsqrlem6  32093  mdsl1i  32269  mdsl2bi  32271  mdexchi  32283  superpos  32302  atabsi  32349  dmdbr5ati  32370  cdj3lem1  32382  fpwrelmapffslem  32684  dp2cl  32829  dpfrac1  32841  cshw1s2  32911  oddpwdc  34338  eulerpartgbij  34356  subfacp1lem2a  35173  subfacp1lem5  35177  subfacp1lem6  35178  subfaclim  35181  sinccvglem  35665  dfon2lem3  35779  dfon2lem7  35783  wsuceq1  35809  clsun  36322  vtoclefex  37328  finxpreclem5  37389  sin2h  37610  cos2h  37611  tan2h  37612  poimirlem22  37642  poimirlem31  37651  opnmbllem0  37656  mblfinlem3  37659  itg2addnclem3  37673  ftc1cnnclem  37691  ftc1anclem6  37698  ftc2nc  37702  dvasin  37704  fdc  37745  constcncf  37762  heiborlem7  37817  atlatmstc  39318  lcmineqlem10  42031  lcmineqlem12  42033  facp2  42136  3rdpwhole  42285  sn-00idlem1  42391  0prjspnlem  42616  sn-isghm  42666  diophren  42806  oaabsb  43287  dftrcl3  43713  dfrtrcl3  43726  cotrclrcl  43735  lhe4.4ex1a  44322  dirkerper  46097  sinnpoly  46895  zlmodzxznm  48502  sinh-conventional  49744