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  1366  equs4  1773  sb4bor  1884  elvd  2817  eueq2dc  2989  sbcgf  3109  csbconstgf  3150  sbcnestg  3191  csbnestg  3192  csbnest1g  3193  ssindif0im  3567  mpteq1  4193  iinexgm  4265  exmid1stab  4320  mss  4341  eusv2nf  4576  eldifpw  4597  ordtriexmid  4642  onsucsssucexmid  4648  ordsucunielexmid  4652  nn0suc  4725  xpss1  4859  xpiindim  4891  reldm0  4973  elrnmpt1s  5006  resdm  5076  resid  5094  eliniseg  5131  trinxp  5155  inimasn  5179  ssrnres  5204  cnveq0  5218  coi2  5278  relrelss  5288  funcnvres  5428  funimaex  5440  fnresin1  5472  fnresin2  5473  fresin  5542  dffv3g  5665  ssimaex  5737  dmfco  5744  fvmpt  5753  fsn  5848  fsn2  5850  funop  5860  elabrex  5929  elabrexg  5930  f1elima  5945  2ndconst  6417  tposfun  6490  tpostpos2  6495  tfrexlem  6564  tfri3  6597  rdgruledefgg  6605  rdgss  6613  frecsuclem  6636  frecrdg  6638  oa0  6689  om0  6690  oei0  6691  oav2  6695  oa1suc  6699  nnmsucr  6720  nnm1  6757  nnm2  6758  ecelqsg  6821  ecidg  6832  xpider  6839  qsel  6845  mapdm0  6896  map0e  6919  mapsnconst  6928  ixpsnf1o  6970  map1  7053  dom1o  7068  xp1en  7073  xpcomco  7076  xpmapenlem  7101  findcard2s  7146  findcard2d  7147  findcard2sd  7148  exmidpw  7167  residfi  7206  fidcenumlemr  7224  sbthlem7  7232  eqinfti  7310  djueq1  7330  omp1eomlem  7384  endjusym  7386  eninl  7387  eninr  7388  difinfsn  7390  finomni  7430  pm54.43  7486  exmidonfinlem  7495  2onetap  7568  mulidpi  7632  nlt1pig  7655  indpi  7656  halfnqq  7724  archnqq  7731  prarloclemarch  7732  prarloclemarch2  7733  nnnq  7736  nq0a0  7771  addpinq1  7778  prarloclemlt  7807  prarloclemlo  7808  prarloclem3  7811  prarloclemcalc  7816  nqprm  7856  addnqpr1  7876  1idprl  7904  1idpru  7905  1idpr  7906  recexprlem1ssl  7947  recexprlem1ssu  7948  ltmprr  7956  0idsr  8081  1idsr  8082  00sr  8083  pn0sr  8085  negexsr  8086  recexgt0sr  8087  ltm1sr  8091  archsr  8096  prsrcl  8098  prsradd  8100  mappsrprg  8118  map2psrprg  8119  elrealeu  8143  pitonnlem1p1  8160  peano2nnnn  8167  ax1rid  8191  axcnre  8195  peano5nnnn  8206  peano2cn  8407  peano2re  8408  addlid  8411  subid  8491  subid1  8492  negid  8519  negeq0  8526  peano2cnm  8538  peano2rem  8539  mul01  8661  lt0neg1  8741  le0neg1  8743  recexre  8851  inelr  8857  rimul  8858  reapmul1  8868  apsqgt0  8874  mulge0  8892  negap0  8903  divvalap  8947  rerecclap  9003  div2negap  9008  divgt0i2i  9190  peano5nni  9239  nnge1  9259  times2  9365  addltmul  9474  nn0p1nn  9534  peano2nn0  9535  nn0lele2xi  9546  fcdmnn0supp  9547  fcdmnn0fsupp  9548  fcdmnn0suppg  9549  znnnlt1  9624  nn0lt10b  9657  prime  9676  msqznn  9677  zeo  9682  elnn1uz2  9938  qreccl  9973  qdivcl  9974  irrmul  9978  rphalfcl  10013  rpnegap  10018  zgt1rpn0n1  10027  ltpnf  10112  nltmnf  10120  pnfge  10121  xlt0neg1  10170  xle0neg1  10172  xaddpnf1  10178  xaddmnf1  10180  xaddid1  10194  xsubge0  10213  xleaddadd  10219  elioopnf  10299  elicopnf  10301  iccshftri  10327  iccshftli  10329  iccdili  10331  icccntri  10333  fzprval  10415  fzofzp1  10571  fzostep1  10582  flqge0nn0  10652  flqge1nn  10653  fldiv4p1lem1div2  10664  exp1  10906  qexpclz  10921  nn0sqcl  10927  expeq0  10931  expubnd  10957  sqval  10958  sqeq0  10963  resqcl  10968  zsqcl  10971  iexpcyc  11005  binom21  11013  bcnn  11118  bcn2  11125  bcn2p1  11131  bcnm1  11133  fihasheq0  11154  hashsng  11159  fihashen1  11160  fimaxq  11190  iswrddm0  11244  ccatval2  11282  ccatsymb  11286  ccatrid  11291  eqs1  11312  s111  11315  swrdnd  11347  pfx00g  11363  shftfibg  11501  shftfib  11504  reim0  11542  imval2  11575  cjap0  11588  cjne0  11589  rexuz3  11671  resqrexlemover  11691  abssq  11762  nn0abscl  11766  nnabscl  11781  abs2dif  11787  max0addsup  11900  climshft  11985  bcxmas  12171  efgt1p2  12377  efgt1p  12378  efi4p  12399  resin4p  12400  recos4p  12401  sinbnd  12434  cosbnd  12435  dvdsval2  12472  zdvdsdc  12494  dvdsmul2  12496  dvdsmulcr  12503  dvdsabseq  12529  divconjdvds  12531  alzdvds  12536  fzo0dvdseq  12539  odd2np1lem  12554  mod2eq1n2dvds  12561  flodddiv4  12618  flodddiv4t2lthalf  12621  bits0  12630  bitsp1o  12635  gcdmndc  12647  gcd0id  12671  gcd1  12679  dfgcd2  12706  gcdmultiple  12712  gcdmultiplez  12713  dvdssq  12723  lcmmndc  12755  lcm0val  12758  dvdslcm  12762  lcmeq0  12764  lcmgcd  12771  lcmdvds  12772  lcmid  12773  lcm1  12774  cncongr2  12797  isprm3  12811  prm2orodd  12819  sqrt2irrap  12873  phiprm  12916  pc0  12998  pcxqcl  13006  pcdvdstr  13021  unennn  13140  ennnfonelemim  13167  ctinfom  13171  ctinf  13173  enctlem  13175  elrestr  13452  tgval  13467  tgvalex  13468  xpsfrnel  13549  xpsfeq  13550  xpscf  13552  mulg1  13838  mulgnegnn  13841  ghmghmrn  13972  subrngintm  14349  subrgintm  14380  lsp0  14563  mulgrhm2  14750  zlmlemg  14768  zlmsca  14772  0opn  14863  topopn  14865  0cld  14969  ntropn  14974  ntrtop  14985  ntr0  14991  neipsm  15011  rest0  15036  xmetres  15239  metres  15240  mopnex  15362  tgioo  15411  cnlimcim  15528  cnlimc  15529  dvfre  15567  dveflem  15583  dvef  15584  efcn  15625  sin2pim  15670  cos2pim  15671  sinmpi  15672  cosmpi  15673  sinppi  15674  cosppi  15675  efimpi  15676  sincosq1lem  15682  sincosq2sgn  15684  sincosq3sgn  15685  sincosq4sgn  15686  sinq12gt0  15687  sinq34lt0t  15688  sincosq1eq  15696  abssinper  15703  logrpap0b  15733  loglt1b  15750  rpcxp0  15755  rpcxp1  15756  rpcxpsqrt  15779  logsqrt  15780  rprelogbdiv  15814  lgs0  15878  lgs2  15882  lgsneg  15889  lgsdilem  15892  lgsdir2lem2  15894  lgsdir2lem4  15896  lgsdir2lem5  15897  lgsne0  15903  2lgslem1a2  15952  2lgslem1c  15955  upgr0eop  16109  uspgrushgr  16167  usgruspgr  16170  usgr0eop  16229  0grsubgr  16251  wlklenvclwlk  16360  upgr2wlkdc  16364  clwwlk0on0  16418  konigsbergssiedgwen  16473  bj-inf2vnlem1  16732  pwle2  16764  pwf1oexmid  16765  domomsubct  16767  nninfsellemeqinf  16786  sbthom  16798  qdiff  16825  iswomninnlem  16826  redc0  16834