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  4264  difexg  4277  rabexg  4281  abssexg  4321  snexg  4323  copsexg  4386  sotritric  4471  sotritrieq  4472  trsuc  4569  oneli  4575  unexb  4590  opeluu  4598  rabxfr  4618  reuhyp  4620  ordunisuc2r  4663  reg3exmid  4729  brrelex12i  4819  brrelex1i  4820  brrelex2i  4821  xpss2  4888  opabid2  4913  eliunxp  4921  releldmi  5023  relelrni  5024  dmexg  5048  rnexg  5049  elres  5101  resexg  5105  relbrcnvg  5169  brcodir  5178  sotri  5186  sotri2  5188  sotri3  5189  dfrel2  5241  coi1  5306  fco  5555  fssres  5568  fabexg  5582  fvopab3g  5781  mptrcl  5791  mpteqb  5799  elfvmptrab1  5804  fvopab4ndm  5806  ffvelcdmi  5845  fsn2  5885  dfmptg  5891  fcof  5897  fvpr1  5922  fvconst2  5934  mptexg  5945  oprabid  6120  ovprc  6124  caovcl  6247  caovass  6253  caovdi  6272  elmpocl  6287  relmptopab  6294  ofexg  6310  resfunexgALT  6341  fo1stresm  6399  fo2ndresm  6400  1stexg  6405  2ndexg  6406  elopabi  6435  mpoexxg  6450  elmpom  6478  supp0  6482  mpoxopn0yelv  6514  rntpos  6532  smores  6567  tfr0dm  6597  tfrlemibxssdm  6602  tfrexlem  6609  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  rdgruledefgg  6650  rdgruledefg  6651  rdgivallem  6656  rdgexg  6664  frec0g  6672  ordgt0ge1  6712  omfnex  6726  oeiv  6733  nna0r  6755  nnm0r  6756  nnsucsssuc  6769  nn2m  6804  nnaordex  6805  nnawordex  6806  ecdmn0m  6855  ecelqsi  6867  ecidg  6877  ectocl  6880  mapfset  6949  encv  7033  f1oen  7050  ssdomg  7070  map1  7106  fiprc  7109  dom1o  7121  xpdom1  7138  fict  7175  isinfinf  7206  ac6sfi  7207  xpfi  7244  en1eqsn  7271  fidcenumlemr  7278  fiss  7317  fipwfi  7328  eqinfti  7367  djueq2  7388  djulclr  7396  djurclr  7397  djulcl  7398  djurcl  7399  djuf1olem  7400  djulclb  7402  inl11  7412  eldju1st  7418  1stinl  7421  2ndinl  7422  1stinr  7423  2ndinr  7424  ctssdccl  7458  isomnimap  7484  ismkvmap  7501  iswomnimap  7513  finacn  7567  djucomen  7579  exmidapne  7633  0nnq  7738  mulidnq  7763  archnqq  7791  prarloclemarch2  7793  nqnq0pi  7812  nq0m0r  7830  nq02m  7839  prarloclemlt  7867  prarloclemn  7873  prarloclem5  7874  addnqprllem  7901  addnqprulem  7902  appdivnq  7937  1idprl  7964  1idpru  7965  addextpr  7995  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemnbj  8041  caucvgprlemloc  8049  caucvgprprlemnbj  8067  caucvgprprlemloc  8077  caucvgprprlemaddq  8082  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemloc  8095  suplocexprlemlub  8098  0nsr  8123  ltsosr  8138  recexgt0sr  8147  prsrpos  8159  caucvgsr  8176  mappsrprg  8178  suplocsrlem  8182  mulresr  8212  axcnre  8255  axpre-ltwlin  8257  mullid  8331  0re  8333  axmulgt0  8404  ltnsym2  8423  eqlei  8427  ltnei  8437  muladd11  8467  cnegex  8512  0cnALT  8524  negcl  8534  negneg  8584  mul02  8722  mulm1  8735  lt0neg2  8805  le0neg2  8807  recexre  8915  recexgt0  8917  mulge0  8956  gt0ap0i  8964  recextlem1  8988  recexap  8990  recclapzi  9076  recap0apzi  9077  recidapzi  9078  divassapzi  9101  divmulapzi  9102  divdirapzi  9103  rerecclapzi  9115  ltp1  9183  recgt0i  9245  ltmul1i  9259  ltdiv1i  9260  ltmuldivi  9261  ltmul2i  9262  lemul1i  9263  lemul2i  9264  sup3exmid  9296  nngt1ne1  9349  nnrecre  9351  nn0ge0  9600  nn0addcl  9610  nn0mulcl  9611  zgt0ge1  9715  dfuzi  9768  eluzel2  9943  eluz2b1  10018  uz2m1nn  10022  elnn0dc  10028  elnndc  10029  nn01to3  10034  zq  10043  nnrecq  10062  rpge0  10085  rpreccl  10099  mnflt  10203  pnfnlt  10207  mnfle  10212  xrlelttr  10226  xrltletr  10227  xrletr  10228  xgepnf  10236  xlt0neg2  10259  xle0neg2  10261  xaddpnf2  10267  xaddmnf2  10269  xaddid2  10283  elioomnf  10388  ige3m2fz  10472  fzshftral  10533  ige2m1fz1  10534  1fv  10564  4fvwrd4  10565  rebtwn2zlemstep  10705  qbtwnxr  10710  btwnzge0  10757  zmodid2  10811  q2txmodxeq0  10843  frec2uzrand  10864  frecuzrdgtcl  10871  frecfzennn  10885  nn0ennn  10892  uzennn  10895  0exp  11033  sqgt0api  11084  subsq2  11106  qsqeqor  11109  bernneq  11120  faclbnd  11202  faclbnd2  11203  faclbnd3  11204  hashinfuni  11239  hashxp  11290  hashpwfi  11292  iswrdiz  11334  lsw0  11375  ccatlid  11397  s1leng  11415  s1fv  11417  s111  11422  pfx0g  11471  2shfti  11619  reim  11640  imcl  11642  crim  11646  caucvgre  11770  rennim  11791  resqrexlemdecn  11801  qabsor  11864  absimle  11874  sqrtthi  11909  sqrtcli  11910  sqrtgt0i  11911  sqrtmsqi  11912  sqrtsqi  11913  sqsqrti  11914  sqrtge0i  11915  absidi  11916  absnidi  11917  xrmaxiflemlub  12040  serclim0  12097  fsum2d  12228  fsumcnv  12230  fsumconst  12247  modfsummodlem1  12249  fsumabs  12258  binom11  12279  prodf1  12335  prodfclim1  12337  prodsnf  12385  fprod2d  12416  fprodcnv  12418  efzval  12476  eftlub  12483  efsep  12484  ef4p  12487  efgt1  12490  reef11  12492  sinf  12497  cosf  12498  efi4p  12510  sinneg  12519  cosneg  12520  efival  12525  efmival  12526  cos01gt0  12556  sin02gt0  12557  absefib  12564  efieq1re  12565  demoivre  12566  demoivreALT  12567  eirraplem  12570  0dvds  12604  odd2np1lem  12665  odd2np1  12666  even2n  12667  mod2eq0even  12671  2teven  12680  opoe  12688  omoe  12689  opeo  12690  omeo  12691  m1exp1  12694  bits0e  12742  bits0o  12743  bitsinv1  12755  gcd0id  12782  gcdid0  12783  1gcd  12795  lcmdvds  12883  isprm2lem  12920  isprm3  12922  prmgt1  12937  coprm  12949  isevengcd2  12963  isoddgcd1  12964  sqpweven  12981  2sqpwodd  12982  sqrtrirr  13015  pythagtriplem12  13084  pythagtriplem13  13085  pythagtriplem14  13086  pythagtriplem16  13088  pc2dvds  13139  oddprmdvds  13163  pockthi  13167  1arith2  13177  prmlem1a  13251  unennn  13347  ctinfomlemom  13377  qnnen  13381  ssnnctlemct  13396  strslfv  13456  slotm  13474  strle1g  13520  1strbas  13531  tgval  13676  ismgmn0  13738  mulgval  13985  mulgfng  13987  mulg0  13988  mulg1  13992  mulg2  13994  isnsg  14065  cntrval  14152  mgpplusg  14330  mgpbas  14333  ringidvalg  14372  ringidval  14373  issrg  14377  subrgpropd  14671  rrgval  14680  islmod  14737  scaffvalg  14753  islssm  14804  sraval  14884  mopnset  14999  metuex  15002  zrhval  15062  zrhvalg  15063  zrhex  15066  asclfval  15131  psrbag  15165  psrbagaddclfi  15175  istopon  15251  eltg4i  15293  eltg3  15295  tg1  15297  tg2  15298  topnex  15324  cldrcl  15340  restsn  15418  lmrcl  15430  metflem  15587  xmetf  15588  ismet2  15592  xmeteq0  15597  xmettri2  15599  xmetpsmet  15607  xmetres2  15617  blfvalps  15623  blex  15625  blvalps  15626  blval  15627  blfps  15647  blf  15648  mopnval  15680  cnbl0  15772  cnblcld  15773  blssioo  15791  resubmet  15794  cncfmet  15830  cnplimcim  15905  cnlimcim  15909  cnlimc  15910  dvfgg  15926  dvfpm  15927  dvfcnpm  15928  dvcj  15947  dvmptfsum  15963  reeff1olem  16009  ef2kpi  16045  sinperlem  16047  sin2kpi  16050  cos2kpi  16051  sinhalfpip  16059  sinhalfpim  16060  coshalfpip  16061  coshalfpim  16062  sincosq1sgn  16065  sinq12gt0  16069  sinkpi  16086  sineq0re  16088  reeflog  16104  relogef  16105  logrpap0b  16118  loggt0b  16133  1cxp  16145  ecxp  16146  2logb9irrap  16225  log2tlbndlog2  16232  log2ublem2  16234  0sgm  16266  chtublem  16307  pcbcctr  16315  bcp1ctr  16318  bclbnd  16319  bposlem1  16323  lgsval2lem  16346  m1lgs  16421  1vgrex  16478  upgrfi  16560  umgredgnlp  16610  wlkop  16806  clwwlkn0  16866  djucllem  17045  bdrabexg  17149  bdunexb  17163  peano5set  17183  speano5  17187  bj-omtrans  17199  pw1ninf  17238  pwf1oexmid  17246  nninfsellemeq  17275  iswomninnlem  17318