Theorem mpan2 422

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 418	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpanr12  436  mp3an23  1319  equs4  1713  sb4bor  1823  elvd  2730  eueq2dc  2898  sbcgf  3017  csbconstgf  3057  sbcnestg  3097  csbnestg  3098  csbnest1g  3099  ssindif0im  3467  mpteq1  4065  iinexgm  4132  mss  4203  eusv2nf  4433  eldifpw  4454  ordtriexmid  4497  onsucsssucexmid  4503  ordsucunielexmid  4507  nn0suc  4580  xpss1  4713  xpiindim  4740  reldm0  4821  elrnmpt1s  4853  resdm  4922  resid  4939  eliniseg  4973  trinxp  4996  inimasn  5020  ssrnres  5045  cnveq0  5059  coi2  5119  relrelss  5129  funcnvres  5260  funimaex  5272  fnresin1  5301  fnresin2  5302  fresin  5365  dffv3g  5481  ssimaex  5546  dmfco  5553  fvmpt  5562  fsn  5656  fsn2  5658  elabrex  5725  f1elima  5740  2ndconst  6186  tposfun  6224  tpostpos2  6229  tfrexlem  6298  tfri3  6331  rdgruledefgg  6339  rdgss  6347  frecsuclem  6370  frecrdg  6372  oa0  6421  om0  6422  oei0  6423  oav2  6427  oa1suc  6431  nnmsucr  6452  nnm1  6488  nnm2  6489  ecelqsg  6550  ecidg  6561  xpider  6568  qsel  6574  mapdm0  6625  map0e  6648  mapsnconst  6656  ixpsnf1o  6698  map1  6774  xp1en  6785  xpcomco  6788  xpmapenlem  6811  findcard2s  6852  findcard2d  6853  findcard2sd  6854  exmidpw  6870  fidcenumlemr  6916  sbthlem7  6924  eqinfti  6981  djueq1  7001  omp1eomlem  7055  endjusym  7057  eninl  7058  eninr  7059  difinfsn  7061  finomni  7100  pm54.43  7142  exmidonfinlem  7145  mulidpi  7255  nlt1pig  7278  indpi  7279  halfnqq  7347  archnqq  7354  prarloclemarch  7355  prarloclemarch2  7356  nnnq  7359  nq0a0  7394  addpinq1  7401  prarloclemlt  7430  prarloclemlo  7431  prarloclem3  7434  prarloclemcalc  7439  nqprm  7479  addnqpr1  7499  1idprl  7527  1idpru  7528  1idpr  7529  recexprlem1ssl  7570  recexprlem1ssu  7571  ltmprr  7579  0idsr  7704  1idsr  7705  00sr  7706  pn0sr  7708  negexsr  7709  recexgt0sr  7710  ltm1sr  7714  archsr  7719  prsrcl  7721  prsradd  7723  mappsrprg  7741  map2psrprg  7742  elrealeu  7766  pitonnlem1p1  7783  peano2nnnn  7790  ax1rid  7814  axcnre  7818  peano5nnnn  7829  peano2cn  8029  peano2re  8030  addid2  8033  subid  8113  subid1  8114  negid  8141  negeq0  8148  peano2cnm  8160  peano2rem  8161  mul01  8283  lt0neg1  8362  le0neg1  8364  recexre  8472  inelr  8478  rimul  8479  reapmul1  8489  apsqgt0  8495  mulge0  8513  negap0  8524  divvalap  8566  rerecclap  8622  div2negap  8627  divgt0i2i  8808  peano5nni  8856  nnge1  8876  times2  8982  addltmul  9089  nn0p1nn  9149  peano2nn0  9150  nn0lele2xi  9161  znnnlt1  9235  nn0lt10b  9267  prime  9286  msqznn  9287  zeo  9292  elnn1uz2  9541  qreccl  9576  qdivcl  9577  irrmul  9581  rphalfcl  9613  rpnegap  9618  zgt1rpn0n1  9627  ltpnf  9712  nltmnf  9720  pnfge  9721  xlt0neg1  9770  xle0neg1  9772  xaddpnf1  9778  xaddmnf1  9780  xaddid1  9794  xsubge0  9813  xleaddadd  9819  elioopnf  9899  elicopnf  9901  iccshftri  9927  iccshftli  9929  iccdili  9931  icccntri  9933  fzprval  10013  fzofzp1  10158  fzostep1  10168  flqge0nn0  10224  flqge1nn  10225  fldiv4p1lem1div2  10236  exp1  10457  qexpclz  10472  nn0sqcl  10478  expeq0  10482  expubnd  10508  sqval  10509  sqeq0  10514  resqcl  10518  zsqcl  10521  iexpcyc  10555  binom21  10563  bcnn  10666  bcn2  10673  bcn2p1  10679  bcnm1  10681  fihasheq0  10703  hashsng  10707  fihashen1  10708  fimaxq  10736  shftfibg  10758  shftfib  10761  reim0  10799  imval2  10832  cjap0  10845  cjne0  10846  rexuz3  10928  resqrexlemover  10948  abssq  11019  nn0abscl  11023  nnabscl  11038  abs2dif  11044  max0addsup  11157  climshft  11241  bcxmas  11426  efgt1p2  11632  efgt1p  11633  efi4p  11654  resin4p  11655  recos4p  11656  sinbnd  11689  cosbnd  11690  dvdsval2  11726  zdvdsdc  11748  dvdsmul2  11750  dvdsmulcr  11757  dvdsabseq  11781  divconjdvds  11783  alzdvds  11788  fzo0dvdseq  11791  odd2np1lem  11805  mod2eq1n2dvds  11812  flodddiv4  11867  flodddiv4t2lthalf  11870  gcdmndc  11873  gcd0id  11908  gcd1  11916  dfgcd2  11943  gcdmultiple  11949  gcdmultiplez  11950  dvdssq  11960  lcmmndc  11990  lcm0val  11993  dvdslcm  11997  lcmeq0  11999  lcmgcd  12006  lcmdvds  12007  lcmid  12008  lcm1  12009  cncongr2  12032  isprm3  12046  prm2orodd  12054  sqrt2irrap  12108  phiprm  12151  pc0  12232  pcdvdstr  12254  unennn  12326  ennnfonelemim  12353  ctinfom  12357  ctinf  12359  enctlem  12361  ressid  12451  elrestr  12559  0opn  12604  topopn  12606  tgval  12649  tgvalex  12650  0cld  12712  ntropn  12717  ntrtop  12728  ntr0  12734  neipsm  12754  rest0  12779  xmetres  12982  metres  12983  mopnex  13105  tgioo  13146  cnlimcim  13240  cnlimc  13241  dvfre  13274  dveflem  13287  dvef  13288  efcn  13289  sin2pim  13334  cos2pim  13335  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  efimpi  13340  sincosq1lem  13346  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  sinq34lt0t  13352  sincosq1eq  13360  abssinper  13367  logrpap0b  13397  loglt1b  13414  rpcxp0  13419  rpcxp1  13420  rpcxpsqrt  13442  logsqrt  13443  rprelogbdiv  13475  lgs0  13514  lgs2  13518  lgsneg  13525  lgsdilem  13528  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdir2lem5  13533  lgsne0  13539  bj-inf2vnlem1  13812  pwle2  13838  pwf1oexmid  13839  exmid1stab  13840  nninfsellemeqinf  13856  sbthom  13865  iswomninnlem  13888  redc0  13896