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  3795  predeq1  6279  wrecseq1  8297  ac6sfi  9238  unfilem1  9261  fiint  9284  ordtypelem2  9479  infxpenc2  9982  dju0en  10136  cfsmolem  10230  axdc4lem  10415  1nqenq  10922  mul02lem1  11357  muleqadd  11829  2halves  12407  halfcl  12415  rehalfcl  12416  half0  12417  halfpos2  12418  halfnneg2  12420  halfaddsub  12422  nneo  12625  zeo  12627  peano5uzi  12630  fztp  13548  uzrdgxfr  13939  bcn2  14291  bcpasc  14293  hashxplem  14405  hashfun  14409  swrds2  14913  repsw2  14923  repsw3  14924  imre  15081  reim  15082  crim  15088  addcj  15121  imval2  15124  cnpart  15213  01sqrexlem7  15221  absmax  15303  binomfallfaclem2  16013  bpoly2  16030  bpoly3  16031  fsumcube  16033  efgt0  16078  sinf  16099  efi4p  16112  resin4p  16113  recos4p  16114  sinneg  16121  efival  16127  cosadd  16140  sinmul  16147  sinbnd  16155  cosbnd  16156  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  rpnnen2lem11  16199  rpnnen2lem12  16200  odd2np1lem  16317  odd2np1  16318  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem15  16807  pythagtriplem16  16808  pythagtriplem17  16809  pockthi  16885  prmreclem5  16898  prmreclem6  16899  prmlem0  17083  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  isghm  19154  odinf  19500  lbsexg  21081  psgnghm2  21497  mopnex  24414  tngnm  24546  tngngp2  24547  tngngpd  24548  tngngp  24549  addccncf  24817  sub1cncf  24819  sub2cncf  24820  iihalf1  24832  iihalf2  24835  pjthlem1  25344  ovolunlem1a  25404  ovolunlem1  25405  opnmbllem  25509  vitalilem4  25519  iblcnlem1  25696  itgcnlem  25698  dvmptre  25880  dvmptim  25881  dvlipcn  25906  mdegldg  25978  aaliou3lem3  26259  aaliou3lem8  26260  sincosq1lem  26413  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  sinq12gt0  26423  abssinper  26437  coskpi  26439  sineq0  26440  coseq1  26441  efeq1  26444  resinf1o  26452  efif1olem2  26459  efif1olem4  26461  logneg2  26531  cxpsqrtlem  26618  cxpsqrt  26619  logsqrt  26620  1cubr  26759  leibpilem2  26858  basellem3  27000  ppiub  27122  chtublem  27129  chtub  27130  bcmax  27196  bcp1ctr  27197  bposlem2  27203  bposlem6  27207  bposlem9  27210  logdivsum  27451  elno  27564  mulscl  28044  4ipval2  30644  ipidsq  30646  dipcl  30648  dipcj  30650  ipasslem11  30776  hvmul0  30960  pjhthlem1  31327  h1de2bi  31490  spanunsni  31515  adjeu  31825  nmopge0  31847  nmfnge0  31863  opsqrlem6  32081  mdsl1i  32257  mdsl2bi  32259  mdexchi  32271  superpos  32290  atabsi  32337  dmdbr5ati  32358  cdj3lem1  32370  fpwrelmapffslem  32662  dp2cl  32807  dpfrac1  32819  cshw1s2  32889  ogrpaddlt  33038  ofldlt1  33298  ofldchr  33299  oddpwdc  34352  eulerpartgbij  34370  subfacp1lem2a  35174  subfacp1lem5  35178  subfacp1lem6  35179  subfaclim  35182  sinccvglem  35666  dfon2lem3  35780  dfon2lem7  35784  wsuceq1  35810  clsun  36323  vtoclefex  37329  finxpreclem5  37390  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem22  37643  poimirlem31  37652  opnmbllem0  37657  mblfinlem3  37660  itg2addnclem3  37674  ftc1cnnclem  37692  ftc1anclem6  37699  ftc2nc  37703  dvasin  37705  fdc  37746  constcncf  37763  heiborlem7  37818  atlatmstc  39319  lcmineqlem10  42033  lcmineqlem12  42035  facp2  42138  3rdpwhole  42287  sn-00idlem1  42393  0prjspnlem  42618  sn-isghm  42668  diophren  42808  oaabsb  43290  dftrcl3  43716  dfrtrcl3  43729  cotrclrcl  43738  lhe4.4ex1a  44325  dirkerper  46101  zlmodzxznm  48490  sinh-conventional  49732