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  1883  elvd  2808  eueq2dc  2980  sbcgf  3100  csbconstgf  3141  sbcnestg  3182  csbnestg  3183  csbnest1g  3184  ssindif0im  3556  mpteq1  4178  iinexgm  4249  exmid1stab  4304  mss  4324  eusv2nf  4559  eldifpw  4580  ordtriexmid  4625  onsucsssucexmid  4631  ordsucunielexmid  4635  nn0suc  4708  xpss1  4842  xpiindim  4873  reldm0  4955  elrnmpt1s  4988  resdm  5058  resid  5076  eliniseg  5113  trinxp  5137  inimasn  5161  ssrnres  5186  cnveq0  5200  coi2  5260  relrelss  5270  funcnvres  5410  funimaex  5422  fnresin1  5454  fnresin2  5455  fresin  5523  dffv3g  5644  ssimaex  5716  dmfco  5723  fvmpt  5732  fsn  5827  fsn2  5829  funop  5839  elabrex  5908  elabrexg  5909  f1elima  5924  2ndconst  6396  tposfun  6469  tpostpos2  6474  tfrexlem  6543  tfri3  6576  rdgruledefgg  6584  rdgss  6592  frecsuclem  6615  frecrdg  6617  oa0  6668  om0  6669  oei0  6670  oav2  6674  oa1suc  6678  nnmsucr  6699  nnm1  6736  nnm2  6737  ecelqsg  6800  ecidg  6811  xpider  6818  qsel  6824  mapdm0  6875  map0e  6898  mapsnconst  6906  ixpsnf1o  6948  map1  7030  dom1o  7045  xp1en  7050  xpcomco  7053  xpmapenlem  7078  findcard2s  7122  findcard2d  7123  findcard2sd  7124  exmidpw  7143  residfi  7182  fidcenumlemr  7197  sbthlem7  7205  eqinfti  7262  djueq1  7282  omp1eomlem  7336  endjusym  7338  eninl  7339  eninr  7340  difinfsn  7342  finomni  7382  pm54.43  7438  exmidonfinlem  7447  2onetap  7517  mulidpi  7581  nlt1pig  7604  indpi  7605  halfnqq  7673  archnqq  7680  prarloclemarch  7681  prarloclemarch2  7682  nnnq  7685  nq0a0  7720  addpinq1  7727  prarloclemlt  7756  prarloclemlo  7757  prarloclem3  7760  prarloclemcalc  7765  nqprm  7805  addnqpr1  7825  1idprl  7853  1idpru  7854  1idpr  7855  recexprlem1ssl  7896  recexprlem1ssu  7897  ltmprr  7905  0idsr  8030  1idsr  8031  00sr  8032  pn0sr  8034  negexsr  8035  recexgt0sr  8036  ltm1sr  8040  archsr  8045  prsrcl  8047  prsradd  8049  mappsrprg  8067  map2psrprg  8068  elrealeu  8092  pitonnlem1p1  8109  peano2nnnn  8116  ax1rid  8140  axcnre  8144  peano5nnnn  8155  peano2cn  8357  peano2re  8358  addlid  8361  subid  8441  subid1  8442  negid  8469  negeq0  8476  peano2cnm  8488  peano2rem  8489  mul01  8611  lt0neg1  8691  le0neg1  8693  recexre  8801  inelr  8807  rimul  8808  reapmul1  8818  apsqgt0  8824  mulge0  8842  negap0  8853  divvalap  8897  rerecclap  8953  div2negap  8958  divgt0i2i  9140  peano5nni  9189  nnge1  9209  times2  9315  addltmul  9424  nn0p1nn  9484  peano2nn0  9485  nn0lele2xi  9496  znnnlt1  9570  nn0lt10b  9603  prime  9622  msqznn  9623  zeo  9628  elnn1uz2  9884  qreccl  9919  qdivcl  9920  irrmul  9924  rphalfcl  9959  rpnegap  9964  zgt1rpn0n1  9973  ltpnf  10058  nltmnf  10066  pnfge  10067  xlt0neg1  10116  xle0neg1  10118  xaddpnf1  10124  xaddmnf1  10126  xaddid1  10140  xsubge0  10159  xleaddadd  10165  elioopnf  10245  elicopnf  10247  iccshftri  10273  iccshftli  10275  iccdili  10277  icccntri  10279  fzprval  10360  fzofzp1  10516  fzostep1  10527  flqge0nn0  10597  flqge1nn  10598  fldiv4p1lem1div2  10609  exp1  10851  qexpclz  10866  nn0sqcl  10872  expeq0  10876  expubnd  10902  sqval  10903  sqeq0  10908  resqcl  10913  zsqcl  10916  iexpcyc  10950  binom21  10958  bcnn  11063  bcn2  11070  bcn2p1  11076  bcnm1  11078  fihasheq0  11099  hashsng  11104  fihashen1  11105  fimaxq  11135  iswrddm0  11184  ccatval2  11222  ccatsymb  11226  ccatrid  11231  eqs1  11252  s111  11255  swrdnd  11287  pfx00g  11303  shftfibg  11441  shftfib  11444  reim0  11482  imval2  11515  cjap0  11528  cjne0  11529  rexuz3  11611  resqrexlemover  11631  abssq  11702  nn0abscl  11706  nnabscl  11721  abs2dif  11727  max0addsup  11840  climshft  11925  bcxmas  12111  efgt1p2  12317  efgt1p  12318  efi4p  12339  resin4p  12340  recos4p  12341  sinbnd  12374  cosbnd  12375  dvdsval2  12412  zdvdsdc  12434  dvdsmul2  12436  dvdsmulcr  12443  dvdsabseq  12469  divconjdvds  12471  alzdvds  12476  fzo0dvdseq  12479  odd2np1lem  12494  mod2eq1n2dvds  12501  flodddiv4  12558  flodddiv4t2lthalf  12561  bits0  12570  bitsp1o  12575  gcdmndc  12587  gcd0id  12611  gcd1  12619  dfgcd2  12646  gcdmultiple  12652  gcdmultiplez  12653  dvdssq  12663  lcmmndc  12695  lcm0val  12698  dvdslcm  12702  lcmeq0  12704  lcmgcd  12711  lcmdvds  12712  lcmid  12713  lcm1  12714  cncongr2  12737  isprm3  12751  prm2orodd  12759  sqrt2irrap  12813  phiprm  12856  pc0  12938  pcxqcl  12946  pcdvdstr  12961  unennn  13079  ennnfonelemim  13106  ctinfom  13110  ctinf  13112  enctlem  13114  elrestr  13391  tgval  13406  tgvalex  13407  xpsfrnel  13488  xpsfeq  13489  xpscf  13491  mulg1  13777  mulgnegnn  13780  ghmghmrn  13911  subrngintm  14288  subrgintm  14319  lsp0  14499  mulgrhm2  14686  zlmlemg  14704  zlmsca  14708  0opn  14797  topopn  14799  0cld  14903  ntropn  14908  ntrtop  14919  ntr0  14925  neipsm  14945  rest0  14970  xmetres  15173  metres  15174  mopnex  15296  tgioo  15345  cnlimcim  15462  cnlimc  15463  dvfre  15501  dveflem  15517  dvef  15518  efcn  15559  sin2pim  15604  cos2pim  15605  sinmpi  15606  cosmpi  15607  sinppi  15608  cosppi  15609  efimpi  15610  sincosq1lem  15616  sincosq2sgn  15618  sincosq3sgn  15619  sincosq4sgn  15620  sinq12gt0  15621  sinq34lt0t  15622  sincosq1eq  15630  abssinper  15637  logrpap0b  15667  loglt1b  15684  rpcxp0  15689  rpcxp1  15690  rpcxpsqrt  15713  logsqrt  15714  rprelogbdiv  15748  lgs0  15812  lgs2  15816  lgsneg  15823  lgsdilem  15826  lgsdir2lem2  15828  lgsdir2lem4  15830  lgsdir2lem5  15831  lgsne0  15837  2lgslem1a2  15886  2lgslem1c  15889  upgr0eop  16043  uspgrushgr  16101  usgruspgr  16104  usgr0eop  16163  0grsubgr  16185  wlklenvclwlk  16294  upgr2wlkdc  16298  clwwlk0on0  16352  konigsbergssiedgwen  16407  bj-inf2vnlem1  16666  pwle2  16700  pwf1oexmid  16701  domomsubct  16703  nninfsellemeqinf  16722  sbthom  16734  qdiff  16761  iswomninnlem  16762  redc0  16770