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	⊢ 𝜓
mpan2.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpan2	⊢ (𝜑 → 𝜒)

Proof of Theorem mpan2

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpan2.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpdan 421	1 ⊢ (𝜑 → 𝜒)

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  1363  equs4  1771  sb4bor  1881  elvd  2805  eueq2dc  2977  sbcgf  3097  csbconstgf  3138  sbcnestg  3179  csbnestg  3180  csbnest1g  3181  ssindif0im  3552  mpteq1  4171  iinexgm  4242  exmid1stab  4296  mss  4316  eusv2nf  4551  eldifpw  4572  ordtriexmid  4617  onsucsssucexmid  4623  ordsucunielexmid  4627  nn0suc  4700  xpss1  4834  xpiindim  4865  reldm0  4947  elrnmpt1s  4980  resdm  5050  resid  5068  eliniseg  5104  trinxp  5128  inimasn  5152  ssrnres  5177  cnveq0  5191  coi2  5251  relrelss  5261  funcnvres  5400  funimaex  5412  fnresin1  5444  fnresin2  5445  fresin  5512  dffv3g  5631  ssimaex  5703  dmfco  5710  fvmpt  5719  fsn  5815  fsn2  5817  funop  5826  elabrex  5893  elabrexg  5894  f1elima  5909  2ndconst  6382  tposfun  6421  tpostpos2  6426  tfrexlem  6495  tfri3  6528  rdgruledefgg  6536  rdgss  6544  frecsuclem  6567  frecrdg  6569  oa0  6620  om0  6621  oei0  6622  oav2  6626  oa1suc  6630  nnmsucr  6651  nnm1  6688  nnm2  6689  ecelqsg  6752  ecidg  6763  xpider  6770  qsel  6776  mapdm0  6827  map0e  6850  mapsnconst  6858  ixpsnf1o  6900  map1  6982  dom1o  6997  xp1en  7002  xpcomco  7005  xpmapenlem  7030  findcard2s  7074  findcard2d  7075  findcard2sd  7076  exmidpw  7095  residfi  7133  fidcenumlemr  7148  sbthlem7  7156  eqinfti  7213  djueq1  7233  omp1eomlem  7287  endjusym  7289  eninl  7290  eninr  7291  difinfsn  7293  finomni  7333  pm54.43  7389  exmidonfinlem  7397  2onetap  7467  mulidpi  7531  nlt1pig  7554  indpi  7555  halfnqq  7623  archnqq  7630  prarloclemarch  7631  prarloclemarch2  7632  nnnq  7635  nq0a0  7670  addpinq1  7677  prarloclemlt  7706  prarloclemlo  7707  prarloclem3  7710  prarloclemcalc  7715  nqprm  7755  addnqpr1  7775  1idprl  7803  1idpru  7804  1idpr  7805  recexprlem1ssl  7846  recexprlem1ssu  7847  ltmprr  7855  0idsr  7980  1idsr  7981  00sr  7982  pn0sr  7984  negexsr  7985  recexgt0sr  7986  ltm1sr  7990  archsr  7995  prsrcl  7997  prsradd  7999  mappsrprg  8017  map2psrprg  8018  elrealeu  8042  pitonnlem1p1  8059  peano2nnnn  8066  ax1rid  8090  axcnre  8094  peano5nnnn  8105  peano2cn  8307  peano2re  8308  addlid  8311  subid  8391  subid1  8392  negid  8419  negeq0  8426  peano2cnm  8438  peano2rem  8439  mul01  8561  lt0neg1  8641  le0neg1  8643  recexre  8751  inelr  8757  rimul  8758  reapmul1  8768  apsqgt0  8774  mulge0  8792  negap0  8803  divvalap  8847  rerecclap  8903  div2negap  8908  divgt0i2i  9090  peano5nni  9139  nnge1  9159  times2  9265  addltmul  9374  nn0p1nn  9434  peano2nn0  9435  nn0lele2xi  9446  znnnlt1  9520  nn0lt10b  9553  prime  9572  msqznn  9573  zeo  9578  elnn1uz2  9834  qreccl  9869  qdivcl  9870  irrmul  9874  rphalfcl  9909  rpnegap  9914  zgt1rpn0n1  9923  ltpnf  10008  nltmnf  10016  pnfge  10017  xlt0neg1  10066  xle0neg1  10068  xaddpnf1  10074  xaddmnf1  10076  xaddid1  10090  xsubge0  10109  xleaddadd  10115  elioopnf  10195  elicopnf  10197  iccshftri  10223  iccshftli  10225  iccdili  10227  icccntri  10229  fzprval  10310  fzofzp1  10465  fzostep1  10476  flqge0nn0  10546  flqge1nn  10547  fldiv4p1lem1div2  10558  exp1  10800  qexpclz  10815  nn0sqcl  10821  expeq0  10825  expubnd  10851  sqval  10852  sqeq0  10857  resqcl  10862  zsqcl  10865  iexpcyc  10899  binom21  10907  bcnn  11012  bcn2  11019  bcn2p1  11025  bcnm1  11027  fihasheq0  11048  hashsng  11053  fihashen1  11054  fimaxq  11084  iswrddm0  11130  ccatval2  11168  ccatsymb  11172  ccatrid  11177  eqs1  11198  s111  11201  swrdnd  11233  pfx00g  11249  shftfibg  11374  shftfib  11377  reim0  11415  imval2  11448  cjap0  11461  cjne0  11462  rexuz3  11544  resqrexlemover  11564  abssq  11635  nn0abscl  11639  nnabscl  11654  abs2dif  11660  max0addsup  11773  climshft  11858  bcxmas  12043  efgt1p2  12249  efgt1p  12250  efi4p  12271  resin4p  12272  recos4p  12273  sinbnd  12306  cosbnd  12307  dvdsval2  12344  zdvdsdc  12366  dvdsmul2  12368  dvdsmulcr  12375  dvdsabseq  12401  divconjdvds  12403  alzdvds  12408  fzo0dvdseq  12411  odd2np1lem  12426  mod2eq1n2dvds  12433  flodddiv4  12490  flodddiv4t2lthalf  12493  bits0  12502  bitsp1o  12507  gcdmndc  12519  gcd0id  12543  gcd1  12551  dfgcd2  12578  gcdmultiple  12584  gcdmultiplez  12585  dvdssq  12595  lcmmndc  12627  lcm0val  12630  dvdslcm  12634  lcmeq0  12636  lcmgcd  12643  lcmdvds  12644  lcmid  12645  lcm1  12646  cncongr2  12669  isprm3  12683  prm2orodd  12691  sqrt2irrap  12745  phiprm  12788  pc0  12870  pcxqcl  12878  pcdvdstr  12893  unennn  13011  ennnfonelemim  13038  ctinfom  13042  ctinf  13044  enctlem  13046  elrestr  13323  tgval  13338  tgvalex  13339  xpsfrnel  13420  xpsfeq  13421  xpscf  13423  mulg1  13709  mulgnegnn  13712  ghmghmrn  13843  subrngintm  14219  subrgintm  14250  lsp0  14430  mulgrhm2  14617  zlmlemg  14635  zlmsca  14639  0opn  14723  topopn  14725  0cld  14829  ntropn  14834  ntrtop  14845  ntr0  14851  neipsm  14871  rest0  14896  xmetres  15099  metres  15100  mopnex  15222  tgioo  15271  cnlimcim  15388  cnlimc  15389  dvfre  15427  dveflem  15443  dvef  15444  efcn  15485  sin2pim  15530  cos2pim  15531  sinmpi  15532  cosmpi  15533  sinppi  15534  cosppi  15535  efimpi  15536  sincosq1lem  15542  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  sinq34lt0t  15548  sincosq1eq  15556  abssinper  15563  logrpap0b  15593  loglt1b  15610  rpcxp0  15615  rpcxp1  15616  rpcxpsqrt  15639  logsqrt  15640  rprelogbdiv  15674  lgs0  15735  lgs2  15739  lgsneg  15746  lgsdilem  15749  lgsdir2lem2  15751  lgsdir2lem4  15753  lgsdir2lem5  15754  lgsne0  15760  2lgslem1a2  15809  2lgslem1c  15812  upgr0eop  15966  uspgrushgr  16024  usgruspgr  16027  usgr0eop  16086  wlklenvclwlk  16184  upgr2wlkdc  16186  clwwlk0on0  16240  bj-inf2vnlem1  16515  pwle2  16549  pwf1oexmid  16550  domomsubct  16552  nninfsellemeqinf  16568  sbthom  16580  iswomninnlem  16603  redc0  16611