Theorem mpan 424

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpan.1	⊢ 𝜑
mpan.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpan	⊢ (𝜓 → 𝜒)

Proof of Theorem mpan

Step	Hyp	Ref	Expression
1		mpan.1	. . 3 ⊢ 𝜑
2	1	a1i 9	. 2 ⊢ (𝜓 → 𝜑)
3		mpan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpancom 422	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:  mp2an  426  mpanl12  436  mp3an1  1360  mp3an12  1363  mp3an13  1364  ax9o  1746  sbnfc2  3188  ssdifss  3337  undifss  3575  uneqdifeqim  3580  elssuni  3921  csbexa  4218  difexg  4231  rabexg  4233  abssexg  4272  snexg  4274  copsexg  4336  sotritric  4421  sotritrieq  4422  trsuc  4519  oneli  4525  unexb  4539  opeluu  4547  rabxfr  4567  reuhyp  4569  ordunisuc2r  4612  reg3exmid  4678  brrelex12i  4768  brrelex1i  4769  brrelex2i  4770  xpss2  4837  opabid2  4861  eliunxp  4869  releldmi  4971  relelrni  4972  dmexg  4996  rnexg  4997  elres  5049  resexg  5053  relbrcnvg  5115  brcodir  5124  sotri  5132  sotri2  5134  sotri3  5135  dfrel2  5187  coi1  5252  fco  5500  fssres  5512  fabexg  5524  fvopab3g  5719  mptrcl  5729  mpteqb  5737  elfvmptrab1  5741  ffvelcdmi  5781  fsn2  5821  dfmptg  5827  fcof  5833  fvpr1  5858  fvconst2  5870  mptexg  5879  oprabid  6050  ovprc  6054  caovcl  6177  caovass  6183  caovdi  6202  elmpocl  6217  relmptopab  6224  ofexg  6240  resfunexgALT  6270  fo1stresm  6324  fo2ndresm  6325  1stexg  6330  2ndexg  6331  elopabi  6360  mpoexxg  6375  elmpom  6403  mpoxopn0yelv  6405  rntpos  6423  smores  6458  tfr0dm  6488  tfrlemibxssdm  6493  tfrexlem  6500  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  rdgruledefgg  6541  rdgruledefg  6542  rdgivallem  6547  rdgexg  6555  frec0g  6563  ordgt0ge1  6603  omfnex  6617  oeiv  6624  nna0r  6646  nnm0r  6647  nnsucsssuc  6660  nn2m  6695  nnaordex  6696  nnawordex  6697  ecdmn0m  6746  ecelqsi  6758  ecidg  6768  ectocl  6771  encv  6915  f1oen  6932  ssdomg  6952  map1  6987  fiprc  6990  dom1o  7002  xpdom1  7019  fict  7055  isinfinf  7086  ac6sfi  7087  xpfi  7124  en1eqsn  7147  fidcenumlemr  7154  fiss  7176  eqinfti  7219  djueq2  7240  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuf1olem  7252  djulclb  7254  inl11  7264  eldju1st  7270  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  ctssdccl  7310  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  finacn  7419  djucomen  7431  exmidapne  7479  0nnq  7584  mulidnq  7609  archnqq  7637  prarloclemarch2  7639  nqnq0pi  7658  nq0m0r  7676  nq02m  7685  prarloclemlt  7713  prarloclemn  7719  prarloclem5  7720  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  1idprl  7810  1idpru  7811  addextpr  7841  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemnbj  7887  caucvgprlemloc  7895  caucvgprprlemnbj  7913  caucvgprprlemloc  7923  caucvgprprlemaddq  7928  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemlub  7944  0nsr  7969  ltsosr  7984  recexgt0sr  7993  prsrpos  8005  caucvgsr  8022  mappsrprg  8024  suplocsrlem  8028  mulresr  8058  axcnre  8101  axpre-ltwlin  8103  mullid  8177  0re  8179  axmulgt0  8251  ltnsym2  8270  eqlei  8273  ltnei  8283  muladd11  8312  cnegex  8357  0cnALT  8369  negcl  8379  negneg  8429  mul02  8566  mulm1  8579  lt0neg2  8649  le0neg2  8651  recexre  8758  recexgt0  8760  mulge0  8799  gt0ap0i  8807  recextlem1  8831  recexap  8833  recclapzi  8917  recap0apzi  8918  recidapzi  8919  divassapzi  8942  divmulapzi  8943  divdirapzi  8944  rerecclapzi  8956  ltp1  9024  recgt0i  9086  ltmul1i  9100  ltdiv1i  9101  ltmuldivi  9102  ltmul2i  9103  lemul1i  9104  lemul2i  9105  sup3exmid  9137  nngt1ne1  9178  nnrecre  9180  nn0ge0  9427  nn0addcl  9437  nn0mulcl  9438  zgt0ge1  9538  dfuzi  9590  eluzel2  9760  eluz2b1  9835  uz2m1nn  9839  elnn0dc  9845  elnndc  9846  nn01to3  9851  zq  9860  nnrecq  9879  rpge0  9901  rpreccl  9915  mnflt  10018  pnfnlt  10022  mnfle  10027  xrlelttr  10041  xrltletr  10042  xrletr  10043  xgepnf  10051  xlt0neg2  10074  xle0neg2  10076  xaddpnf2  10082  xaddmnf2  10084  xaddid2  10098  elioomnf  10203  ige3m2fz  10284  fzshftral  10343  ige2m1fz1  10344  1fv  10374  4fvwrd4  10375  rebtwn2zlemstep  10513  qbtwnxr  10518  btwnzge0  10561  zmodid2  10615  q2txmodxeq0  10647  frec2uzrand  10668  frecuzrdgtcl  10675  frecfzennn  10689  nn0ennn  10696  uzennn  10699  0exp  10837  sqgt0api  10888  subsq2  10910  qsqeqor  10913  bernneq  10923  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  hashinfuni  11040  hashxp  11091  iswrdiz  11121  lsw0  11162  ccatlid  11184  s1leng  11202  s1fv  11204  s111  11209  pfx0g  11258  2shfti  11393  reim  11414  imcl  11416  crim  11420  caucvgre  11543  rennim  11564  resqrexlemdecn  11574  qabsor  11637  absimle  11646  sqrtthi  11681  sqrtcli  11682  sqrtgt0i  11683  sqrtmsqi  11684  sqrtsqi  11685  sqsqrti  11686  sqrtge0i  11687  absidi  11688  absnidi  11689  xrmaxiflemlub  11810  serclim0  11867  fsum2d  11998  fsumcnv  12000  fsumconst  12017  modfsummodlem1  12019  fsumabs  12028  binom11  12049  prodf1  12105  prodfclim1  12107  prodsnf  12155  fprod2d  12186  fprodcnv  12188  efzval  12246  eftlub  12253  efsep  12254  ef4p  12257  efgt1  12260  reef11  12262  sinf  12267  cosf  12268  efi4p  12280  sinneg  12289  cosneg  12290  efival  12295  efmival  12296  cos01gt0  12326  sin02gt0  12327  absefib  12334  efieq1re  12335  demoivre  12336  demoivreALT  12337  eirraplem  12340  0dvds  12374  odd2np1lem  12435  odd2np1  12436  even2n  12437  mod2eq0even  12441  2teven  12450  opoe  12458  omoe  12459  opeo  12460  omeo  12461  m1exp1  12464  bits0e  12512  bits0o  12513  bitsinv1  12525  gcd0id  12552  gcdid0  12553  1gcd  12565  lcmdvds  12653  isprm2lem  12690  isprm3  12692  prmgt1  12706  coprm  12718  isevengcd2  12732  isoddgcd1  12733  sqpweven  12749  2sqpwodd  12750  pythagtriplem12  12850  pythagtriplem13  12851  pythagtriplem14  12852  pythagtriplem16  12854  pc2dvds  12905  oddprmdvds  12929  pockthi  12933  1arith2  12943  unennn  13020  ctinfomlemom  13050  qnnen  13054  ssnnctlemct  13069  strslfv  13129  strle1g  13191  1strbas  13202  tgval  13347  ismgmn0  13443  mulgval  13711  mulgfng  13713  mulg0  13714  mulg1  13718  mulg2  13720  isnsg  13791  ringidvalg  13977  issrg  13981  subrgpropd  14270  rrgval  14279  islmod  14308  scaffvalg  14323  islssm  14374  sraval  14454  mopnset  14569  metuex  14572  zrhval  14634  zrhvalg  14635  zrhex  14638  psrbag  14686  istopon  14740  eltg4i  14782  eltg3  14784  tg1  14786  tg2  14787  topnex  14813  cldrcl  14829  restsn  14907  lmrcl  14919  metflem  15076  xmetf  15077  ismet2  15081  xmeteq0  15086  xmettri2  15088  xmetpsmet  15096  xmetres2  15106  blfvalps  15112  blex  15114  blvalps  15115  blval  15116  blfps  15136  blf  15137  mopnval  15169  cnbl0  15261  cnblcld  15262  blssioo  15280  resubmet  15283  cncfmet  15319  cnplimcim  15394  cnlimcim  15398  cnlimc  15399  dvfgg  15415  dvfpm  15416  dvfcnpm  15417  dvcj  15436  dvmptfsum  15452  reeff1olem  15498  ef2kpi  15533  sinperlem  15535  sin2kpi  15538  cos2kpi  15539  sinhalfpip  15547  sinhalfpim  15548  coshalfpip  15549  coshalfpim  15550  sincosq1sgn  15553  sinq12gt0  15557  sinkpi  15574  reeflog  15590  relogef  15591  logrpap0b  15603  loggt0b  15618  1cxp  15627  ecxp  15628  2logb9irrap  15704  0sgm  15712  lgsval2lem  15742  m1lgs  15817  1vgrex  15874  upgrfi  15956  umgredgnlp  16006  wlkop  16202  clwwlkn0  16262  djucllem  16417  bdrabexg  16522  bdunexb  16536  peano5set  16556  speano5  16560  bj-omtrans  16572  pw1ninf  16611  pwf1oexmid  16621  nninfsellemeq  16637  iswomninnlem  16674