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  1329  equs4  1725  sb4bor  1835  elvd  2743  eueq2dc  2911  sbcgf  3031  csbconstgf  3071  sbcnestg  3111  csbnestg  3112  csbnest1g  3113  ssindif0im  3483  mpteq1  4088  iinexgm  4155  exmid1stab  4209  mss  4227  eusv2nf  4457  eldifpw  4478  ordtriexmid  4521  onsucsssucexmid  4527  ordsucunielexmid  4531  nn0suc  4604  xpss1  4737  xpiindim  4765  reldm0  4846  elrnmpt1s  4878  resdm  4947  resid  4965  eliniseg  4999  trinxp  5023  inimasn  5047  ssrnres  5072  cnveq0  5086  coi2  5146  relrelss  5156  funcnvres  5290  funimaex  5302  fnresin1  5331  fnresin2  5332  fresin  5395  dffv3g  5512  ssimaex  5578  dmfco  5585  fvmpt  5594  fsn  5689  fsn2  5691  elabrex  5759  f1elima  5774  2ndconst  6223  tposfun  6261  tpostpos2  6266  tfrexlem  6335  tfri3  6368  rdgruledefgg  6376  rdgss  6384  frecsuclem  6407  frecrdg  6409  oa0  6458  om0  6459  oei0  6460  oav2  6464  oa1suc  6468  nnmsucr  6489  nnm1  6526  nnm2  6527  ecelqsg  6588  ecidg  6599  xpider  6606  qsel  6612  mapdm0  6663  map0e  6686  mapsnconst  6694  ixpsnf1o  6736  map1  6812  xp1en  6823  xpcomco  6826  xpmapenlem  6849  findcard2s  6890  findcard2d  6891  findcard2sd  6892  exmidpw  6908  fidcenumlemr  6954  sbthlem7  6962  eqinfti  7019  djueq1  7039  omp1eomlem  7093  endjusym  7095  eninl  7096  eninr  7097  difinfsn  7099  finomni  7138  pm54.43  7189  exmidonfinlem  7192  2onetap  7254  mulidpi  7317  nlt1pig  7340  indpi  7341  halfnqq  7409  archnqq  7416  prarloclemarch  7417  prarloclemarch2  7418  nnnq  7421  nq0a0  7456  addpinq1  7463  prarloclemlt  7492  prarloclemlo  7493  prarloclem3  7496  prarloclemcalc  7501  nqprm  7541  addnqpr1  7561  1idprl  7589  1idpru  7590  1idpr  7591  recexprlem1ssl  7632  recexprlem1ssu  7633  ltmprr  7641  0idsr  7766  1idsr  7767  00sr  7768  pn0sr  7770  negexsr  7771  recexgt0sr  7772  ltm1sr  7776  archsr  7781  prsrcl  7783  prsradd  7785  mappsrprg  7803  map2psrprg  7804  elrealeu  7828  pitonnlem1p1  7845  peano2nnnn  7852  ax1rid  7876  axcnre  7880  peano5nnnn  7891  peano2cn  8092  peano2re  8093  addlid  8096  subid  8176  subid1  8177  negid  8204  negeq0  8211  peano2cnm  8223  peano2rem  8224  mul01  8346  lt0neg1  8425  le0neg1  8427  recexre  8535  inelr  8541  rimul  8542  reapmul1  8552  apsqgt0  8558  mulge0  8576  negap0  8587  divvalap  8631  rerecclap  8687  div2negap  8692  divgt0i2i  8874  peano5nni  8922  nnge1  8942  times2  9048  addltmul  9155  nn0p1nn  9215  peano2nn0  9216  nn0lele2xi  9227  znnnlt1  9301  nn0lt10b  9333  prime  9352  msqznn  9353  zeo  9358  elnn1uz2  9607  qreccl  9642  qdivcl  9643  irrmul  9647  rphalfcl  9681  rpnegap  9686  zgt1rpn0n1  9695  ltpnf  9780  nltmnf  9788  pnfge  9789  xlt0neg1  9838  xle0neg1  9840  xaddpnf1  9846  xaddmnf1  9848  xaddid1  9862  xsubge0  9881  xleaddadd  9887  elioopnf  9967  elicopnf  9969  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  fzprval  10082  fzofzp1  10227  fzostep1  10237  flqge0nn0  10293  flqge1nn  10294  fldiv4p1lem1div2  10305  exp1  10526  qexpclz  10541  nn0sqcl  10547  expeq0  10551  expubnd  10577  sqval  10578  sqeq0  10583  resqcl  10588  zsqcl  10591  iexpcyc  10625  binom21  10633  bcnn  10737  bcn2  10744  bcn2p1  10750  bcnm1  10752  fihasheq0  10773  hashsng  10778  fihashen1  10779  fimaxq  10807  shftfibg  10829  shftfib  10832  reim0  10870  imval2  10903  cjap0  10916  cjne0  10917  rexuz3  10999  resqrexlemover  11019  abssq  11090  nn0abscl  11094  nnabscl  11109  abs2dif  11115  max0addsup  11228  climshft  11312  bcxmas  11497  efgt1p2  11703  efgt1p  11704  efi4p  11725  resin4p  11726  recos4p  11727  sinbnd  11760  cosbnd  11761  dvdsval2  11797  zdvdsdc  11819  dvdsmul2  11821  dvdsmulcr  11828  dvdsabseq  11853  divconjdvds  11855  alzdvds  11860  fzo0dvdseq  11863  odd2np1lem  11877  mod2eq1n2dvds  11884  flodddiv4  11939  flodddiv4t2lthalf  11942  gcdmndc  11945  gcd0id  11980  gcd1  11988  dfgcd2  12015  gcdmultiple  12021  gcdmultiplez  12022  dvdssq  12032  lcmmndc  12062  lcm0val  12065  dvdslcm  12069  lcmeq0  12071  lcmgcd  12078  lcmdvds  12079  lcmid  12080  lcm1  12081  cncongr2  12104  isprm3  12118  prm2orodd  12126  sqrt2irrap  12180  phiprm  12223  pc0  12304  pcdvdstr  12326  unennn  12398  ennnfonelemim  12425  ctinfom  12429  ctinf  12431  enctlem  12433  elrestr  12696  tgval  12711  tgvalex  12712  xpsfrnel  12763  xpsfeq  12764  xpscf  12766  mulg1  12990  mulgnegnn  12993  subrgintm  13364  0opn  13509  topopn  13511  0cld  13615  ntropn  13620  ntrtop  13631  ntr0  13637  neipsm  13657  rest0  13682  xmetres  13885  metres  13886  mopnex  14008  tgioo  14049  cnlimcim  14143  cnlimc  14144  dvfre  14177  dveflem  14190  dvef  14191  efcn  14192  sin2pim  14237  cos2pim  14238  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  efimpi  14243  sincosq1lem  14249  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  sinq34lt0t  14255  sincosq1eq  14263  abssinper  14270  logrpap0b  14300  loglt1b  14317  rpcxp0  14322  rpcxp1  14323  rpcxpsqrt  14345  logsqrt  14346  rprelogbdiv  14378  lgs0  14417  lgs2  14421  lgsneg  14428  lgsdilem  14431  lgsdir2lem2  14433  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsne0  14442  bj-inf2vnlem1  14725  pwle2  14751  pwf1oexmid  14752  nninfsellemeqinf  14768  sbthom  14777  iswomninnlem  14800  redc0  14808