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  3789  predeq1  6265  wrecseq1  8272  ac6sfi  9208  unfilem1  9231  fiint  9254  ordtypelem2  9449  infxpenc2  9954  dju0en  10108  cfsmolem  10202  axdc4lem  10387  1nqenq  10894  mul02lem1  11329  muleqadd  11801  2halves  12379  halfcl  12387  rehalfcl  12388  half0  12389  halfpos2  12390  halfnneg2  12392  halfaddsub  12394  nneo  12597  zeo  12599  peano5uzi  12602  fztp  13520  uzrdgxfr  13911  bcn2  14263  bcpasc  14265  hashxplem  14377  hashfun  14381  swrds2  14884  repsw2  14894  repsw3  14895  imre  15052  reim  15053  crim  15059  addcj  15092  imval2  15095  cnpart  15184  01sqrexlem7  15192  absmax  15274  binomfallfaclem2  15984  bpoly2  16001  bpoly3  16002  fsumcube  16004  efgt0  16049  sinf  16070  efi4p  16083  resin4p  16084  recos4p  16085  sinneg  16092  efival  16098  cosadd  16111  sinmul  16118  sinbnd  16126  cosbnd  16127  ef01bndlem  16130  sin01bnd  16131  cos01bnd  16132  sin01gt0  16136  cos01gt0  16137  sin02gt0  16138  rpnnen2lem11  16170  rpnnen2lem12  16171  odd2np1lem  16288  odd2np1  16289  pythagtriplem12  16775  pythagtriplem14  16777  pythagtriplem15  16778  pythagtriplem16  16779  pythagtriplem17  16780  pockthi  16856  prmreclem5  16869  prmreclem6  16870  prmlem0  17054  prdsplusg  17399  prdsmulr  17400  prdsvsca  17401  isghm  19131  odinf  19479  ogrpaddlt  20054  ofldlt1  20797  lbsexg  21108  ofldchr  21520  psgnghm2  21525  mopnex  24442  tngnm  24574  tngngp2  24575  tngngpd  24576  tngngp  24577  addccncf  24845  sub1cncf  24847  sub2cncf  24848  iihalf1  24860  iihalf2  24863  pjthlem1  25372  ovolunlem1a  25432  ovolunlem1  25433  opnmbllem  25537  vitalilem4  25547  iblcnlem1  25724  itgcnlem  25726  dvmptre  25908  dvmptim  25909  dvlipcn  25934  mdegldg  26006  aaliou3lem3  26287  aaliou3lem8  26288  sincosq1lem  26441  sincosq2sgn  26443  sincosq3sgn  26444  sincosq4sgn  26445  sinq12gt0  26451  abssinper  26465  coskpi  26467  sineq0  26468  coseq1  26469  efeq1  26472  resinf1o  26480  efif1olem2  26487  efif1olem4  26489  logneg2  26559  cxpsqrtlem  26646  cxpsqrt  26647  logsqrt  26648  1cubr  26787  leibpilem2  26886  basellem3  27028  ppiub  27150  chtublem  27157  chtub  27158  bcmax  27224  bcp1ctr  27225  bposlem2  27231  bposlem6  27235  bposlem9  27238  logdivsum  27479  elno  27592  mulscl  28079  4ipval2  30689  ipidsq  30691  dipcl  30693  dipcj  30695  ipasslem11  30821  hvmul0  31005  pjhthlem1  31372  h1de2bi  31535  spanunsni  31560  adjeu  31870  nmopge0  31892  nmfnge0  31908  opsqrlem6  32126  mdsl1i  32302  mdsl2bi  32304  mdexchi  32316  superpos  32335  atabsi  32382  dmdbr5ati  32403  cdj3lem1  32415  fpwrelmapffslem  32707  dp2cl  32852  dpfrac1  32864  cshw1s2  32934  oddpwdc  34340  eulerpartgbij  34358  subfacp1lem2a  35162  subfacp1lem5  35166  subfacp1lem6  35167  subfaclim  35170  sinccvglem  35654  dfon2lem3  35768  dfon2lem7  35772  wsuceq1  35798  clsun  36311  vtoclefex  37317  finxpreclem5  37378  sin2h  37599  cos2h  37600  tan2h  37601  poimirlem22  37631  poimirlem31  37640  opnmbllem0  37645  mblfinlem3  37648  itg2addnclem3  37662  ftc1cnnclem  37680  ftc1anclem6  37687  ftc2nc  37691  dvasin  37693  fdc  37734  constcncf  37751  heiborlem7  37806  atlatmstc  39307  lcmineqlem10  42021  lcmineqlem12  42023  facp2  42126  3rdpwhole  42275  sn-00idlem1  42381  0prjspnlem  42606  sn-isghm  42656  diophren  42796  oaabsb  43278  dftrcl3  43704  dfrtrcl3  43717  cotrclrcl  43726  lhe4.4ex1a  44313  dirkerper  46089  sinnpoly  46887  zlmodzxznm  48481  sinh-conventional  49723