Theorem mpan 428

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 426	1 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp2an  430  mpanl12  440  mp3an1  1365  mp3an12  1368  mp3an13  1369  ax9o  1750  sbnfc2  3208  ssdifss  3359  undifss  3608  uneqdifeqim  3613  elssuni  3963  csbexa  4262  difexg  4275  rabexg  4279  abssexg  4319  snexg  4321  copsexg  4384  sotritric  4469  sotritrieq  4470  trsuc  4567  oneli  4573  unexb  4588  opeluu  4596  rabxfr  4616  reuhyp  4618  ordunisuc2r  4661  reg3exmid  4727  brrelex12i  4817  brrelex1i  4818  brrelex2i  4819  xpss2  4886  opabid2  4911  eliunxp  4919  releldmi  5021  relelrni  5022  dmexg  5046  rnexg  5047  elres  5099  resexg  5103  relbrcnvg  5166  brcodir  5175  sotri  5183  sotri2  5185  sotri3  5186  dfrel2  5238  coi1  5303  fco  5552  fssres  5565  fabexg  5579  fvopab3g  5778  mptrcl  5788  mpteqb  5796  elfvmptrab1  5801  fvopab4ndm  5803  ffvelcdmi  5842  fsn2  5882  dfmptg  5888  fcof  5894  fvpr1  5919  fvconst2  5931  mptexg  5942  oprabid  6117  ovprc  6121  caovcl  6244  caovass  6250  caovdi  6269  elmpocl  6284  relmptopab  6291  ofexg  6307  resfunexgALT  6337  fo1stresm  6395  fo2ndresm  6396  1stexg  6401  2ndexg  6402  elopabi  6431  mpoexxg  6446  elmpom  6474  supp0  6478  mpoxopn0yelv  6510  rntpos  6528  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfrexlem  6605  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  rdgruledefgg  6646  rdgruledefg  6647  rdgivallem  6652  rdgexg  6660  frec0g  6668  ordgt0ge1  6708  omfnex  6722  oeiv  6729  nna0r  6751  nnm0r  6752  nnsucsssuc  6765  nn2m  6800  nnaordex  6801  nnawordex  6802  ecdmn0m  6851  ecelqsi  6863  ecidg  6873  ectocl  6876  mapfset  6945  encv  7028  f1oen  7045  ssdomg  7065  map1  7101  fiprc  7104  dom1o  7116  xpdom1  7133  fict  7170  isinfinf  7201  ac6sfi  7202  xpfi  7239  en1eqsn  7265  fidcenumlemr  7272  fiss  7311  fipwfi  7321  eqinfti  7360  djueq2  7381  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djuf1olem  7393  djulclb  7395  inl11  7405  eldju1st  7411  1stinl  7414  2ndinl  7415  1stinr  7416  2ndinr  7417  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  finacn  7560  djucomen  7572  exmidapne  7626  0nnq  7731  mulidnq  7756  archnqq  7784  prarloclemarch2  7786  nqnq0pi  7805  nq0m0r  7823  nq02m  7832  prarloclemlt  7860  prarloclemn  7866  prarloclem5  7867  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  1idprl  7957  1idpru  7958  addextpr  7988  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemnbj  8034  caucvgprlemloc  8042  caucvgprprlemnbj  8060  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemlub  8091  0nsr  8116  ltsosr  8131  recexgt0sr  8140  prsrpos  8152  caucvgsr  8169  mappsrprg  8171  suplocsrlem  8175  mulresr  8205  axcnre  8248  axpre-ltwlin  8250  mullid  8324  0re  8326  axmulgt0  8397  ltnsym2  8416  eqlei  8419  ltnei  8429  muladd11  8459  cnegex  8504  0cnALT  8516  negcl  8526  negneg  8576  mul02  8714  mulm1  8727  lt0neg2  8797  le0neg2  8799  recexre  8907  recexgt0  8909  mulge0  8948  gt0ap0i  8956  recextlem1  8980  recexap  8982  recclapzi  9068  recap0apzi  9069  recidapzi  9070  divassapzi  9093  divmulapzi  9094  divdirapzi  9095  rerecclapzi  9107  ltp1  9175  recgt0i  9237  ltmul1i  9251  ltdiv1i  9252  ltmuldivi  9253  ltmul2i  9254  lemul1i  9255  lemul2i  9256  sup3exmid  9288  nngt1ne1  9340  nnrecre  9342  nn0ge0  9590  nn0addcl  9600  nn0mulcl  9601  zgt0ge1  9705  dfuzi  9758  eluzel2  9928  eluz2b1  10003  uz2m1nn  10007  elnn0dc  10013  elnndc  10014  nn01to3  10019  zq  10028  nnrecq  10047  rpge0  10069  rpreccl  10083  mnflt  10187  pnfnlt  10191  mnfle  10196  xrlelttr  10210  xrltletr  10211  xrletr  10212  xgepnf  10220  xlt0neg2  10243  xle0neg2  10245  xaddpnf2  10251  xaddmnf2  10253  xaddid2  10267  elioomnf  10372  ige3m2fz  10456  fzshftral  10517  ige2m1fz1  10518  1fv  10548  4fvwrd4  10549  rebtwn2zlemstep  10689  qbtwnxr  10694  btwnzge0  10737  zmodid2  10791  q2txmodxeq0  10823  frec2uzrand  10844  frecuzrdgtcl  10851  frecfzennn  10865  nn0ennn  10872  uzennn  10875  0exp  11013  sqgt0api  11064  subsq2  11086  qsqeqor  11089  bernneq  11100  faclbnd  11181  faclbnd2  11182  faclbnd3  11183  hashinfuni  11218  hashxp  11269  hashpwfi  11271  iswrdiz  11313  lsw0  11354  ccatlid  11376  s1leng  11394  s1fv  11396  s111  11401  pfx0g  11450  2shfti  11598  reim  11619  imcl  11621  crim  11625  caucvgre  11749  rennim  11770  resqrexlemdecn  11780  qabsor  11843  absimle  11852  sqrtthi  11887  sqrtcli  11888  sqrtgt0i  11889  sqrtmsqi  11890  sqrtsqi  11891  sqsqrti  11892  sqrtge0i  11893  absidi  11894  absnidi  11895  xrmaxiflemlub  12016  serclim0  12073  fsum2d  12204  fsumcnv  12206  fsumconst  12223  modfsummodlem1  12225  fsumabs  12234  binom11  12255  prodf1  12311  prodfclim1  12313  prodsnf  12361  fprod2d  12392  fprodcnv  12394  efzval  12452  eftlub  12459  efsep  12460  ef4p  12463  efgt1  12466  reef11  12468  sinf  12473  cosf  12474  efi4p  12486  sinneg  12495  cosneg  12496  efival  12501  efmival  12502  cos01gt0  12532  sin02gt0  12533  absefib  12540  efieq1re  12541  demoivre  12542  demoivreALT  12543  eirraplem  12546  0dvds  12580  odd2np1lem  12641  odd2np1  12642  even2n  12643  mod2eq0even  12647  2teven  12656  opoe  12664  omoe  12665  opeo  12666  omeo  12667  m1exp1  12670  bits0e  12718  bits0o  12719  bitsinv1  12731  gcd0id  12758  gcdid0  12759  1gcd  12771  lcmdvds  12859  isprm2lem  12896  isprm3  12898  prmgt1  12912  coprm  12924  isevengcd2  12938  isoddgcd1  12939  sqpweven  12955  2sqpwodd  12956  pythagtriplem12  13056  pythagtriplem13  13057  pythagtriplem14  13058  pythagtriplem16  13060  pc2dvds  13111  oddprmdvds  13135  pockthi  13139  1arith2  13149  unennn  13290  ctinfomlemom  13320  qnnen  13324  ssnnctlemct  13339  strslfv  13399  slotm  13417  strle1g  13462  1strbas  13473  tgval  13618  ismgmn0  13680  mulgval  13927  mulgfng  13929  mulg0  13930  mulg1  13934  mulg2  13936  isnsg  14007  mgpplusg  14224  mgpbas  14227  ringidvalg  14266  ringidval  14267  issrg  14271  subrgpropd  14563  rrgval  14572  islmod  14629  scaffvalg  14645  islssm  14696  sraval  14776  mopnset  14891  metuex  14894  zrhval  14954  zrhvalg  14955  zrhex  14958  asclfval  15023  psrbag  15055  psrbagaddclfi  15063  istopon  15116  eltg4i  15158  eltg3  15160  tg1  15162  tg2  15163  topnex  15189  cldrcl  15205  restsn  15283  lmrcl  15295  metflem  15452  xmetf  15453  ismet2  15457  xmeteq0  15462  xmettri2  15464  xmetpsmet  15472  xmetres2  15482  blfvalps  15488  blex  15490  blvalps  15491  blval  15492  blfps  15512  blf  15513  mopnval  15545  cnbl0  15637  cnblcld  15638  blssioo  15656  resubmet  15659  cncfmet  15695  cnplimcim  15770  cnlimcim  15774  cnlimc  15775  dvfgg  15791  dvfpm  15792  dvfcnpm  15793  dvcj  15812  dvmptfsum  15828  reeff1olem  15874  ef2kpi  15910  sinperlem  15912  sin2kpi  15915  cos2kpi  15916  sinhalfpip  15924  sinhalfpim  15925  coshalfpip  15926  coshalfpim  15927  sincosq1sgn  15930  sinq12gt0  15934  sinkpi  15951  reeflog  15967  relogef  15968  logrpap0b  15981  loggt0b  15996  1cxp  16008  ecxp  16009  2logb9irrap  16085  log2tlbndlog2  16088  log2ublem2  16090  0sgm  16105  pcbcctr  16123  bcp1ctr  16126  bclbnd  16127  lgsval2lem  16141  m1lgs  16216  1vgrex  16273  upgrfi  16355  umgredgnlp  16405  wlkop  16601  clwwlkn0  16661  djucllem  16840  bdrabexg  16944  bdunexb  16958  peano5set  16978  speano5  16982  bj-omtrans  16994  pw1ninf  17033  pwf1oexmid  17041  nninfsellemeq  17069  iswomninnlem  17111