Theorem mpd3an3 1425

Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)

Hypotheses

Ref	Expression
mpd3an3.2	|- ( ( ph /\ ps ) -> ch )
mpd3an3.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mpd3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mpd3an3

Step	Hyp	Ref	Expression
1		mpd3an3.2	. 2 |- ( ( ph /\ ps ) -> ch )
2		mpd3an3.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1265	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpdan 702	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  stoic2b  1700  elovmpt2  6879  f1oeng  7974  wdomimag  8492  cdaval  8992  gruuni  9622  genpv  9821  infssuzle  11771  fzrevral3  12427  flflp1  12608  subsq2  12973  brfi1ind  13281  opfi1ind  13284  brfi1indOLD  13287  opfi1indOLD  13290  ccatws1ls  13410  swrdrlen  13435  swrd0swrdid  13464  2cshwid  13560  caubnd  14098  dvdsmul1  15003  dvdsmul2  15004  hashbcval  15706  setsvalg  15887  ressval  15927  restval  16087  mrelatglb0  17185  imasmnd2  17327  qusinv  17653  ghminv  17667  symgov  17810  gexod  18001  lsmvalx  18054  ringrz  18588  imasring  18619  irredneg  18710  evlrhm  19525  gsumsmonply1  19673  ocvin  20018  frlmiscvec  20188  mat1mhm  20290  marrepfval  20366  marrepval0  20367  marepvfval  20371  marepvval0  20372  1elcpmat  20520  m2cpminv0  20566  idpm2idmp  20606  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  restin  20970  qtopval  21498  elqtop3  21506  elfm3  21754  flimval  21767  nmge0  22421  nmeq0  22422  nminv  22425  nmo0  22539  0nghm  22545  coemulhi  24010  isosctrlem2  24549  divsqrtsumlem  24706  2lgsoddprmlem4  25140  0uhgrrusgr  26474  frgruhgr0v  27127  nvge0  27528  nvnd  27543  dip0r  27572  dip0l  27573  nmoo0  27646  hi2eq  27962  resvval  29827  unitdivcld  29947  signspval  30629  ltflcei  33397  elghomlem1OLD  33684  rngorz  33722  rngonegmn1l  33740  rngonegmn1r  33741  igenval  33860  lfl0  34352  olj01  34512  olm11  34514  hl2at  34691  pmapeq0  35052  trlcl  35451  trlle  35471  tendoid  36061  tendo0plr  36080  tendoipl2  36086  erngmul  36094  erngmul-rN  36102  dvamulr  36300  dvavadd  36303  dvhmulr  36375  cdlemm10N  36407  pellfund14  37462  mendmulr  37758  fmuldfeq  39815  stoweidlem19  40236  stoweidlem26  40243  pfxpfxid  41416  pfxcctswrd  41417  prelspr  41736  lincval1  42208