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  2804  eueq2dc  2976  sbcgf  3096  csbconstgf  3137  sbcnestg  3178  csbnestg  3179  csbnest1g  3180  ssindif0im  3551  mpteq1  4167  iinexgm  4237  exmid1stab  4291  mss  4311  eusv2nf  4546  eldifpw  4567  ordtriexmid  4612  onsucsssucexmid  4618  ordsucunielexmid  4622  nn0suc  4695  xpss1  4828  xpiindim  4858  reldm0  4940  elrnmpt1s  4973  resdm  5043  resid  5061  eliniseg  5097  trinxp  5121  inimasn  5145  ssrnres  5170  cnveq0  5184  coi2  5244  relrelss  5254  funcnvres  5393  funimaex  5405  fnresin1  5437  fnresin2  5438  fresin  5503  dffv3g  5622  ssimaex  5694  dmfco  5701  fvmpt  5710  fsn  5806  fsn2  5808  funop  5817  elabrex  5880  elabrexg  5881  f1elima  5896  2ndconst  6366  tposfun  6404  tpostpos2  6409  tfrexlem  6478  tfri3  6511  rdgruledefgg  6519  rdgss  6527  frecsuclem  6550  frecrdg  6552  oa0  6601  om0  6602  oei0  6603  oav2  6607  oa1suc  6611  nnmsucr  6632  nnm1  6669  nnm2  6670  ecelqsg  6733  ecidg  6744  xpider  6751  qsel  6757  mapdm0  6808  map0e  6831  mapsnconst  6839  ixpsnf1o  6881  map1  6963  xp1en  6978  xpcomco  6981  xpmapenlem  7006  findcard2s  7048  findcard2d  7049  findcard2sd  7050  exmidpw  7066  residfi  7103  fidcenumlemr  7118  sbthlem7  7126  eqinfti  7183  djueq1  7203  omp1eomlem  7257  endjusym  7259  eninl  7260  eninr  7261  difinfsn  7263  finomni  7303  pm54.43  7359  exmidonfinlem  7367  2onetap  7437  mulidpi  7501  nlt1pig  7524  indpi  7525  halfnqq  7593  archnqq  7600  prarloclemarch  7601  prarloclemarch2  7602  nnnq  7605  nq0a0  7640  addpinq1  7647  prarloclemlt  7676  prarloclemlo  7677  prarloclem3  7680  prarloclemcalc  7685  nqprm  7725  addnqpr1  7745  1idprl  7773  1idpru  7774  1idpr  7775  recexprlem1ssl  7816  recexprlem1ssu  7817  ltmprr  7825  0idsr  7950  1idsr  7951  00sr  7952  pn0sr  7954  negexsr  7955  recexgt0sr  7956  ltm1sr  7960  archsr  7965  prsrcl  7967  prsradd  7969  mappsrprg  7987  map2psrprg  7988  elrealeu  8012  pitonnlem1p1  8029  peano2nnnn  8036  ax1rid  8060  axcnre  8064  peano5nnnn  8075  peano2cn  8277  peano2re  8278  addlid  8281  subid  8361  subid1  8362  negid  8389  negeq0  8396  peano2cnm  8408  peano2rem  8409  mul01  8531  lt0neg1  8611  le0neg1  8613  recexre  8721  inelr  8727  rimul  8728  reapmul1  8738  apsqgt0  8744  mulge0  8762  negap0  8773  divvalap  8817  rerecclap  8873  div2negap  8878  divgt0i2i  9060  peano5nni  9109  nnge1  9129  times2  9235  addltmul  9344  nn0p1nn  9404  peano2nn0  9405  nn0lele2xi  9416  znnnlt1  9490  nn0lt10b  9523  prime  9542  msqznn  9543  zeo  9548  elnn1uz2  9798  qreccl  9833  qdivcl  9834  irrmul  9838  rphalfcl  9873  rpnegap  9878  zgt1rpn0n1  9887  ltpnf  9972  nltmnf  9980  pnfge  9981  xlt0neg1  10030  xle0neg1  10032  xaddpnf1  10038  xaddmnf1  10040  xaddid1  10054  xsubge0  10073  xleaddadd  10079  elioopnf  10159  elicopnf  10161  iccshftri  10187  iccshftli  10189  iccdili  10191  icccntri  10193  fzprval  10274  fzofzp1  10428  fzostep1  10438  flqge0nn0  10508  flqge1nn  10509  fldiv4p1lem1div2  10520  exp1  10762  qexpclz  10777  nn0sqcl  10783  expeq0  10787  expubnd  10813  sqval  10814  sqeq0  10819  resqcl  10824  zsqcl  10827  iexpcyc  10861  binom21  10869  bcnn  10974  bcn2  10981  bcn2p1  10987  bcnm1  10989  fihasheq0  11010  hashsng  11015  fihashen1  11016  fimaxq  11044  iswrddm0  11090  ccatval2  11128  ccatsymb  11132  ccatrid  11137  eqs1  11156  s111  11159  swrdnd  11186  pfx00g  11202  shftfibg  11326  shftfib  11329  reim0  11367  imval2  11400  cjap0  11413  cjne0  11414  rexuz3  11496  resqrexlemover  11516  abssq  11587  nn0abscl  11591  nnabscl  11606  abs2dif  11612  max0addsup  11725  climshft  11810  bcxmas  11995  efgt1p2  12201  efgt1p  12202  efi4p  12223  resin4p  12224  recos4p  12225  sinbnd  12258  cosbnd  12259  dvdsval2  12296  zdvdsdc  12318  dvdsmul2  12320  dvdsmulcr  12327  dvdsabseq  12353  divconjdvds  12355  alzdvds  12360  fzo0dvdseq  12363  odd2np1lem  12378  mod2eq1n2dvds  12385  flodddiv4  12442  flodddiv4t2lthalf  12445  bits0  12454  bitsp1o  12459  gcdmndc  12471  gcd0id  12495  gcd1  12503  dfgcd2  12530  gcdmultiple  12536  gcdmultiplez  12537  dvdssq  12547  lcmmndc  12579  lcm0val  12582  dvdslcm  12586  lcmeq0  12588  lcmgcd  12595  lcmdvds  12596  lcmid  12597  lcm1  12598  cncongr2  12621  isprm3  12635  prm2orodd  12643  sqrt2irrap  12697  phiprm  12740  pc0  12822  pcxqcl  12830  pcdvdstr  12845  unennn  12963  ennnfonelemim  12990  ctinfom  12994  ctinf  12996  enctlem  12998  elrestr  13275  tgval  13290  tgvalex  13291  xpsfrnel  13372  xpsfeq  13373  xpscf  13375  mulg1  13661  mulgnegnn  13664  ghmghmrn  13795  subrngintm  14170  subrgintm  14201  lsp0  14381  mulgrhm2  14568  zlmlemg  14586  zlmsca  14590  0opn  14674  topopn  14676  0cld  14780  ntropn  14785  ntrtop  14796  ntr0  14802  neipsm  14822  rest0  14847  xmetres  15050  metres  15051  mopnex  15173  tgioo  15222  cnlimcim  15339  cnlimc  15340  dvfre  15378  dveflem  15394  dvef  15395  efcn  15436  sin2pim  15481  cos2pim  15482  sinmpi  15483  cosmpi  15484  sinppi  15485  cosppi  15486  efimpi  15487  sincosq1lem  15493  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  sinq34lt0t  15499  sincosq1eq  15507  abssinper  15514  logrpap0b  15544  loglt1b  15561  rpcxp0  15566  rpcxp1  15567  rpcxpsqrt  15590  logsqrt  15591  rprelogbdiv  15625  lgs0  15686  lgs2  15690  lgsneg  15697  lgsdilem  15700  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsne0  15711  2lgslem1a2  15760  2lgslem1c  15763  upgr0eop  15916  uspgrushgr  15972  usgruspgr  15975  bj-inf2vnlem1  16291  dom1o  16314  pwle2  16323  pwf1oexmid  16324  domomsubct  16326  nninfsellemeqinf  16341  sbthom  16353  iswomninnlem  16376  redc0  16384