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  3775  predeq1  6250  wrecseq1  8245  ac6sfi  9168  unfilem1  9189  fiint  9211  ordtypelem2  9405  infxpenc2  9913  dju0en  10067  cfsmolem  10161  axdc4lem  10346  1nqenq  10853  mul02lem1  11289  muleqadd  11761  2halves  12339  halfcl  12347  rehalfcl  12348  half0  12349  halfpos2  12350  halfnneg2  12352  halfaddsub  12354  nneo  12557  zeo  12559  peano5uzi  12562  fztp  13480  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  19127  odinf  19475  ogrpaddlt  20050  ofldlt1  20790  lbsexg  21101  ofldchr  21513  psgnghm2  21518  mopnex  24434  tngnm  24566  tngngp2  24567  tngngpd  24568  tngngp  24569  addccncf  24837  sub1cncf  24839  sub2cncf  24840  iihalf1  24852  iihalf2  24855  pjthlem1  25364  ovolunlem1a  25424  ovolunlem1  25425  opnmbllem  25529  vitalilem4  25539  iblcnlem1  25716  itgcnlem  25718  dvmptre  25900  dvmptim  25901  dvlipcn  25926  mdegldg  25998  aaliou3lem3  26279  aaliou3lem8  26280  sincosq1lem  26433  sincosq2sgn  26435  sincosq3sgn  26436  sincosq4sgn  26437  sinq12gt0  26443  abssinper  26457  coskpi  26459  sineq0  26460  coseq1  26461  efeq1  26464  resinf1o  26472  efif1olem2  26479  efif1olem4  26481  logneg2  26551  cxpsqrtlem  26638  cxpsqrt  26639  logsqrt  26640  1cubr  26779  leibpilem2  26878  basellem3  27020  ppiub  27142  chtublem  27149  chtub  27150  bcmax  27216  bcp1ctr  27217  bposlem2  27223  bposlem6  27227  bposlem9  27230  logdivsum  27471  elno  27584  mulscl  28073  4ipval2  30688  ipidsq  30690  dipcl  30692  dipcj  30694  ipasslem11  30820  hvmul0  31004  pjhthlem1  31371  h1de2bi  31534  spanunsni  31559  adjeu  31869  nmopge0  31891  nmfnge0  31907  opsqrlem6  32125  mdsl1i  32301  mdsl2bi  32303  mdexchi  32315  superpos  32334  atabsi  32381  dmdbr5ati  32402  cdj3lem1  32414  fpwrelmapffslem  32715  dp2cl  32860  dpfrac1  32872  cshw1s2  32941  oddpwdc  34367  eulerpartgbij  34385  subfacp1lem2a  35224  subfacp1lem5  35228  subfacp1lem6  35229  subfaclim  35232  sinccvglem  35716  dfon2lem3  35827  dfon2lem7  35831  wsuceq1  35857  clsun  36372  vtoclefex  37378  finxpreclem5  37439  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem22  37681  poimirlem31  37690  opnmbllem0  37695  mblfinlem3  37698  itg2addnclem3  37712  ftc1cnnclem  37730  ftc1anclem6  37737  ftc2nc  37741  dvasin  37743  fdc  37784  constcncf  37801  heiborlem7  37856  atlatmstc  39417  lcmineqlem10  42130  lcmineqlem12  42132  facp2  42235  3rdpwhole  42384  sn-00idlem1  42490  0prjspnlem  42715  sn-isghm  42765  diophren  42905  oaabsb  43386  dftrcl3  43812  dfrtrcl3  43825  cotrclrcl  43834  lhe4.4ex1a  44421  dirkerper  46193  sinnpoly  46990  zlmodzxznm  48597  sinh-conventional  49839