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  4168  iinexgm  4239  exmid1stab  4293  mss  4313  eusv2nf  4548  eldifpw  4569  ordtriexmid  4614  onsucsssucexmid  4620  ordsucunielexmid  4624  nn0suc  4697  xpss1  4831  xpiindim  4862  reldm0  4944  elrnmpt1s  4977  resdm  5047  resid  5065  eliniseg  5101  trinxp  5125  inimasn  5149  ssrnres  5174  cnveq0  5188  coi2  5248  relrelss  5258  funcnvres  5397  funimaex  5409  fnresin1  5441  fnresin2  5442  fresin  5509  dffv3g  5628  ssimaex  5700  dmfco  5707  fvmpt  5716  fsn  5812  fsn2  5814  funop  5823  elabrex  5890  elabrexg  5891  f1elima  5906  2ndconst  6379  tposfun  6417  tpostpos2  6422  tfrexlem  6491  tfri3  6524  rdgruledefgg  6532  rdgss  6540  frecsuclem  6563  frecrdg  6565  oa0  6616  om0  6617  oei0  6618  oav2  6622  oa1suc  6626  nnmsucr  6647  nnm1  6684  nnm2  6685  ecelqsg  6748  ecidg  6759  xpider  6766  qsel  6772  mapdm0  6823  map0e  6846  mapsnconst  6854  ixpsnf1o  6896  map1  6978  dom1o  6990  xp1en  6995  xpcomco  6998  xpmapenlem  7023  findcard2s  7065  findcard2d  7066  findcard2sd  7067  exmidpw  7086  residfi  7123  fidcenumlemr  7138  sbthlem7  7146  eqinfti  7203  djueq1  7223  omp1eomlem  7277  endjusym  7279  eninl  7280  eninr  7281  difinfsn  7283  finomni  7323  pm54.43  7379  exmidonfinlem  7387  2onetap  7457  mulidpi  7521  nlt1pig  7544  indpi  7545  halfnqq  7613  archnqq  7620  prarloclemarch  7621  prarloclemarch2  7622  nnnq  7625  nq0a0  7660  addpinq1  7667  prarloclemlt  7696  prarloclemlo  7697  prarloclem3  7700  prarloclemcalc  7705  nqprm  7745  addnqpr1  7765  1idprl  7793  1idpru  7794  1idpr  7795  recexprlem1ssl  7836  recexprlem1ssu  7837  ltmprr  7845  0idsr  7970  1idsr  7971  00sr  7972  pn0sr  7974  negexsr  7975  recexgt0sr  7976  ltm1sr  7980  archsr  7985  prsrcl  7987  prsradd  7989  mappsrprg  8007  map2psrprg  8008  elrealeu  8032  pitonnlem1p1  8049  peano2nnnn  8056  ax1rid  8080  axcnre  8084  peano5nnnn  8095  peano2cn  8297  peano2re  8298  addlid  8301  subid  8381  subid1  8382  negid  8409  negeq0  8416  peano2cnm  8428  peano2rem  8429  mul01  8551  lt0neg1  8631  le0neg1  8633  recexre  8741  inelr  8747  rimul  8748  reapmul1  8758  apsqgt0  8764  mulge0  8782  negap0  8793  divvalap  8837  rerecclap  8893  div2negap  8898  divgt0i2i  9080  peano5nni  9129  nnge1  9149  times2  9255  addltmul  9364  nn0p1nn  9424  peano2nn0  9425  nn0lele2xi  9436  znnnlt1  9510  nn0lt10b  9543  prime  9562  msqznn  9563  zeo  9568  elnn1uz2  9819  qreccl  9854  qdivcl  9855  irrmul  9859  rphalfcl  9894  rpnegap  9899  zgt1rpn0n1  9908  ltpnf  9993  nltmnf  10001  pnfge  10002  xlt0neg1  10051  xle0neg1  10053  xaddpnf1  10059  xaddmnf1  10061  xaddid1  10075  xsubge0  10094  xleaddadd  10100  elioopnf  10180  elicopnf  10182  iccshftri  10208  iccshftli  10210  iccdili  10212  icccntri  10214  fzprval  10295  fzofzp1  10450  fzostep1  10460  flqge0nn0  10530  flqge1nn  10531  fldiv4p1lem1div2  10542  exp1  10784  qexpclz  10799  nn0sqcl  10805  expeq0  10809  expubnd  10835  sqval  10836  sqeq0  10841  resqcl  10846  zsqcl  10849  iexpcyc  10883  binom21  10891  bcnn  10996  bcn2  11003  bcn2p1  11009  bcnm1  11011  fihasheq0  11032  hashsng  11037  fihashen1  11038  fimaxq  11067  iswrddm0  11113  ccatval2  11151  ccatsymb  11155  ccatrid  11160  eqs1  11181  s111  11184  swrdnd  11212  pfx00g  11228  shftfibg  11352  shftfib  11355  reim0  11393  imval2  11426  cjap0  11439  cjne0  11440  rexuz3  11522  resqrexlemover  11542  abssq  11613  nn0abscl  11617  nnabscl  11632  abs2dif  11638  max0addsup  11751  climshft  11836  bcxmas  12021  efgt1p2  12227  efgt1p  12228  efi4p  12249  resin4p  12250  recos4p  12251  sinbnd  12284  cosbnd  12285  dvdsval2  12322  zdvdsdc  12344  dvdsmul2  12346  dvdsmulcr  12353  dvdsabseq  12379  divconjdvds  12381  alzdvds  12386  fzo0dvdseq  12389  odd2np1lem  12404  mod2eq1n2dvds  12411  flodddiv4  12468  flodddiv4t2lthalf  12471  bits0  12480  bitsp1o  12485  gcdmndc  12497  gcd0id  12521  gcd1  12529  dfgcd2  12556  gcdmultiple  12562  gcdmultiplez  12563  dvdssq  12573  lcmmndc  12605  lcm0val  12608  dvdslcm  12612  lcmeq0  12614  lcmgcd  12621  lcmdvds  12622  lcmid  12623  lcm1  12624  cncongr2  12647  isprm3  12661  prm2orodd  12669  sqrt2irrap  12723  phiprm  12766  pc0  12848  pcxqcl  12856  pcdvdstr  12871  unennn  12989  ennnfonelemim  13016  ctinfom  13020  ctinf  13022  enctlem  13024  elrestr  13301  tgval  13316  tgvalex  13317  xpsfrnel  13398  xpsfeq  13399  xpscf  13401  mulg1  13687  mulgnegnn  13690  ghmghmrn  13821  subrngintm  14197  subrgintm  14228  lsp0  14408  mulgrhm2  14595  zlmlemg  14613  zlmsca  14617  0opn  14701  topopn  14703  0cld  14807  ntropn  14812  ntrtop  14823  ntr0  14829  neipsm  14849  rest0  14874  xmetres  15077  metres  15078  mopnex  15200  tgioo  15249  cnlimcim  15366  cnlimc  15367  dvfre  15405  dveflem  15421  dvef  15422  efcn  15463  sin2pim  15508  cos2pim  15509  sinmpi  15510  cosmpi  15511  sinppi  15512  cosppi  15513  efimpi  15514  sincosq1lem  15520  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  sinq34lt0t  15526  sincosq1eq  15534  abssinper  15541  logrpap0b  15571  loglt1b  15588  rpcxp0  15593  rpcxp1  15594  rpcxpsqrt  15617  logsqrt  15618  rprelogbdiv  15652  lgs0  15713  lgs2  15717  lgsneg  15724  lgsdilem  15727  lgsdir2lem2  15729  lgsdir2lem4  15731  lgsdir2lem5  15732  lgsne0  15738  2lgslem1a2  15787  2lgslem1c  15790  upgr0eop  15943  uspgrushgr  15999  usgruspgr  16002  usgr0eop  16061  wlklenvclwlk  16145  upgr2wlkdc  16147  bj-inf2vnlem1  16442  pwle2  16477  pwf1oexmid  16478  domomsubct  16480  nninfsellemeqinf  16496  sbthom  16508  iswomninnlem  16531  redc0  16539