Theorem mpan2 425

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)

Hypotheses

Ref	Expression
mpan2.1	|- ps
mpan2.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpan2	|- ( ph -> ch )

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpan2.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	2, 3	mpdan 421	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpanr12  439  mp3an23  1366  equs4  1773  sb4bor  1884  elvd  2820  eueq2dc  2993  sbcgf  3113  csbconstgf  3154  sbcnestg  3195  csbnestg  3196  csbnest1g  3197  ssindif0im  3572  mpteq1  4199  iinexgm  4271  exmid1stab  4326  mss  4347  eusv2nf  4582  eldifpw  4603  ordtriexmid  4648  onsucsssucexmid  4654  ordsucunielexmid  4658  nn0suc  4731  xpss1  4865  xpiindim  4897  reldm0  4979  elrnmpt1s  5012  resdm  5082  resid  5100  eliniseg  5137  trinxp  5161  inimasn  5185  ssrnres  5210  cnveq0  5224  coi2  5284  relrelss  5294  funcnvres  5434  funimaex  5446  fnresin1  5478  fnresin2  5479  fresin  5548  dffv3g  5671  ssimaex  5743  dmfco  5750  fvmpt  5759  fsn  5854  fsn2  5856  funop  5866  elabrex  5936  elabrexg  5937  f1elima  5952  2ndconst  6431  tposfun  6504  tpostpos2  6509  tfrexlem  6578  tfri3  6611  rdgruledefgg  6619  rdgss  6627  frecsuclem  6650  frecrdg  6652  oa0  6703  om0  6704  oei0  6705  oav2  6709  oa1suc  6713  nnmsucr  6734  nnm1  6771  nnm2  6772  ecelqsg  6835  ecidg  6846  xpider  6853  qsel  6859  mapdm0  6910  map0e  6933  mapsnconst  6942  ixpsnf1o  6984  map1  7067  dom1o  7082  xp1en  7087  xpcomco  7090  xpmapenlem  7115  findcard2s  7160  findcard2d  7161  findcard2sd  7162  exmidpw  7181  residfi  7220  fidcenumlemr  7238  sbthlem7  7246  eqinfti  7324  djueq1  7344  omp1eomlem  7398  endjusym  7400  eninl  7401  eninr  7402  difinfsn  7404  finomni  7444  pm54.43  7500  exmidonfinlem  7509  2onetap  7585  mulidpi  7649  nlt1pig  7672  indpi  7673  halfnqq  7741  archnqq  7748  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  nq0a0  7788  addpinq1  7795  prarloclemlt  7824  prarloclemlo  7825  prarloclem3  7828  prarloclemcalc  7833  nqprm  7873  addnqpr1  7893  1idprl  7921  1idpru  7922  1idpr  7923  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  0idsr  8098  1idsr  8099  00sr  8100  pn0sr  8102  negexsr  8103  recexgt0sr  8104  ltm1sr  8108  archsr  8113  prsrcl  8115  prsradd  8117  mappsrprg  8135  map2psrprg  8136  elrealeu  8160  pitonnlem1p1  8177  peano2nnnn  8184  ax1rid  8208  axcnre  8212  peano5nnnn  8223  peano2cn  8424  peano2re  8425  addlid  8428  subid  8508  subid1  8509  negid  8536  negeq0  8543  peano2cnm  8555  peano2rem  8556  mul01  8679  lt0neg1  8759  le0neg1  8761  recexre  8869  inelr  8875  rimul  8876  reapmul1  8886  apsqgt0  8892  mulge0  8910  negap0  8921  divvalap  8965  rerecclap  9021  div2negap  9026  divgt0i2i  9208  peano5nni  9257  nnge1  9277  times2  9383  addltmul  9492  nn0p1nn  9552  peano2nn0  9553  nn0lele2xi  9564  fcdmnn0supp  9565  fcdmnn0fsupp  9566  fcdmnn0suppg  9567  znnnlt1  9642  nn0lt10b  9676  prime  9695  msqznn  9696  zeo  9701  elnn1uz2  9957  qreccl  9992  qdivcl  9993  irrmul  9997  rphalfcl  10032  rpnegap  10037  zgt1rpn0n1  10046  ltpnf  10132  nltmnf  10140  pnfge  10141  xlt0neg1  10190  xle0neg1  10192  xaddpnf1  10198  xaddmnf1  10200  xaddid1  10214  xsubge0  10233  xleaddadd  10239  elioopnf  10319  elicopnf  10321  iccshftri  10347  iccshftli  10349  iccdili  10351  icccntri  10353  fzprval  10438  fzofzp1  10594  fzostep1  10605  flqge0nn0  10677  flqge1nn  10678  fldiv4p1lem1div2  10689  exp1  10931  qexpclz  10946  nn0sqcl  10952  expeq0  10956  expubnd  10982  sqval  10983  sqeq0  10988  resqcl  10993  zsqcl  10996  iexpcyc  11030  binom21  11038  bcnn  11144  bcn2  11151  bcn2p1  11158  bcnm1  11160  fihasheq0  11181  hashsng  11186  fihashen1  11187  fimaxq  11219  iswrddm0  11273  ccatval2  11311  ccatsymb  11315  ccatrid  11320  eqs1  11341  s111  11344  swrdnd  11376  pfx00g  11392  shftfibg  11530  shftfib  11533  reim0  11571  imval2  11604  cjap0  11617  cjne0  11618  rexuz3  11700  resqrexlemover  11720  abssq  11791  nn0abscl  11795  nnabscl  11810  abs2dif  11816  max0addsup  11929  climshft  12014  bcxmas  12200  efgt1p2  12406  efgt1p  12407  efi4p  12428  resin4p  12429  recos4p  12430  sinbnd  12463  cosbnd  12464  dvdsval2  12501  zdvdsdc  12523  dvdsmul2  12525  dvdsmulcr  12532  dvdsabseq  12558  divconjdvds  12560  alzdvds  12565  fzo0dvdseq  12568  odd2np1lem  12583  mod2eq1n2dvds  12590  flodddiv4  12647  flodddiv4t2lthalf  12650  bits0  12659  bitsp1o  12664  gcdmndc  12676  gcd0id  12700  gcd1  12708  dfgcd2  12735  gcdmultiple  12741  gcdmultiplez  12742  dvdssq  12752  lcmmndc  12784  lcm0val  12787  dvdslcm  12791  lcmeq0  12793  lcmgcd  12800  lcmdvds  12801  lcmid  12802  lcm1  12803  cncongr2  12826  isprm3  12840  prm2orodd  12848  sqrt2irrap  12902  phiprm  12945  pc0  13027  pcxqcl  13035  pcdvdstr  13050  ballotfilem2  13172  ballotfilemfcc  13177  ballotfilem4  13185  unennn  13232  ennnfonelemim  13259  ctinfom  13263  ctinf  13265  enctlem  13267  elrestr  13544  tgval  13559  tgvalex  13560  xpsfrnel  13608  xpsfeq  13609  xpscf  13611  mulg1  13882  mulgnegnn  13885  ghmghmrn  14016  subrngintm  14458  subrgintm  14489  lsp0  14697  mulgrhm2  14884  zlmlemg  14902  zlmsca  14906  0opn  14997  topopn  14999  0cld  15103  ntropn  15108  ntrtop  15119  ntr0  15125  neipsm  15145  rest0  15170  xmetres  15373  metres  15374  mopnex  15496  tgioo  15545  cnlimcim  15662  cnlimc  15663  dvfre  15701  dveflem  15717  dvef  15718  efcn  15759  sin2pim  15804  cos2pim  15805  sinmpi  15806  cosmpi  15807  sinppi  15808  cosppi  15809  efimpi  15810  sincosq1lem  15816  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  sinq34lt0t  15822  sincosq1eq  15830  abssinper  15837  logrpap0b  15867  loglt1b  15884  rpcxp0  15889  rpcxp1  15890  rpcxpsqrt  15913  logsqrt  15914  rprelogbdiv  15948  lgs0  16012  lgs2  16016  lgsneg  16023  lgsdilem  16026  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsne0  16037  2lgslem1a2  16086  2lgslem1c  16089  upgr0eop  16243  uspgrushgr  16301  usgruspgr  16304  usgr0eop  16363  0grsubgr  16385  wlklenvclwlk  16494  upgr2wlkdc  16498  clwwlk0on0  16552  konigsbergssiedgwen  16607  bj-inf2vnlem1  16866  pwle2  16898  pwf1oexmid  16899  domomsubct  16901  nninfsellemeqinf  16920  sbthom  16932  qdiff  16959  iswomninnlem  16960  redc0  16968