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  1361  mp3an12  1364  mp3an13  1365  ax9o  1746  sbnfc2  3202  ssdifss  3353  undifss  3594  uneqdifeqim  3599  elssuni  3947  csbexa  4244  difexg  4257  rabexg  4260  abssexg  4300  snexg  4302  copsexg  4365  sotritric  4450  sotritrieq  4451  trsuc  4548  oneli  4554  unexb  4568  opeluu  4576  rabxfr  4596  reuhyp  4598  ordunisuc2r  4641  reg3exmid  4707  brrelex12i  4797  brrelex1i  4798  brrelex2i  4799  xpss2  4866  opabid2  4891  eliunxp  4899  releldmi  5001  relelrni  5002  dmexg  5026  rnexg  5027  elres  5079  resexg  5083  relbrcnvg  5146  brcodir  5155  sotri  5163  sotri2  5165  sotri3  5166  dfrel2  5218  coi1  5283  fco  5532  fssres  5545  fabexg  5559  fvopab3g  5755  mptrcl  5765  mpteqb  5773  elfvmptrab1  5777  ffvelcdmi  5816  fsn2  5856  dfmptg  5862  fcof  5868  fvpr1  5893  fvconst2  5905  mptexg  5916  oprabid  6090  ovprc  6094  caovcl  6217  caovass  6223  caovdi  6242  elmpocl  6257  relmptopab  6264  ofexg  6280  resfunexgALT  6310  fo1stresm  6368  fo2ndresm  6369  1stexg  6374  2ndexg  6375  elopabi  6404  mpoexxg  6419  elmpom  6447  supp0  6451  mpoxopn0yelv  6483  rntpos  6501  smores  6536  tfr0dm  6566  tfrlemibxssdm  6571  tfrexlem  6578  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  rdgruledefgg  6619  rdgruledefg  6620  rdgivallem  6625  rdgexg  6633  frec0g  6641  ordgt0ge1  6681  omfnex  6695  oeiv  6702  nna0r  6724  nnm0r  6725  nnsucsssuc  6738  nn2m  6773  nnaordex  6774  nnawordex  6775  ecdmn0m  6824  ecelqsi  6836  ecidg  6846  ectocl  6849  encv  6994  f1oen  7011  ssdomg  7031  map1  7067  fiprc  7070  dom1o  7082  xpdom1  7099  fict  7136  isinfinf  7167  ac6sfi  7168  xpfi  7205  en1eqsn  7231  fidcenumlemr  7238  fiss  7277  fipwfi  7285  eqinfti  7324  djueq2  7345  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djuf1olem  7357  djulclb  7359  inl11  7369  eldju1st  7375  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  ctssdccl  7415  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  finacn  7524  djucomen  7536  exmidapne  7590  0nnq  7695  mulidnq  7720  archnqq  7748  prarloclemarch2  7750  nqnq0pi  7769  nq0m0r  7787  nq02m  7796  prarloclemlt  7824  prarloclemn  7830  prarloclem5  7831  addnqprllem  7858  addnqprulem  7859  appdivnq  7894  1idprl  7921  1idpru  7922  addextpr  7952  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemnbj  7998  caucvgprlemloc  8006  caucvgprprlemnbj  8024  caucvgprprlemloc  8034  caucvgprprlemaddq  8039  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemlub  8055  0nsr  8080  ltsosr  8095  recexgt0sr  8104  prsrpos  8116  caucvgsr  8133  mappsrprg  8135  suplocsrlem  8139  mulresr  8169  axcnre  8212  axpre-ltwlin  8214  mullid  8288  0re  8290  axmulgt0  8361  ltnsym2  8380  eqlei  8383  ltnei  8393  muladd11  8423  cnegex  8468  0cnALT  8480  negcl  8490  negneg  8540  mul02  8678  mulm1  8691  lt0neg2  8761  le0neg2  8763  recexre  8870  recexgt0  8872  mulge0  8911  gt0ap0i  8919  recextlem1  8943  recexap  8945  recclapzi  9031  recap0apzi  9032  recidapzi  9033  divassapzi  9056  divmulapzi  9057  divdirapzi  9058  rerecclapzi  9070  ltp1  9138  recgt0i  9200  ltmul1i  9214  ltdiv1i  9215  ltmuldivi  9216  ltmul2i  9217  lemul1i  9218  lemul2i  9219  sup3exmid  9251  nngt1ne1  9292  nnrecre  9294  nn0ge0  9541  nn0addcl  9551  nn0mulcl  9552  zgt0ge1  9656  dfuzi  9709  eluzel2  9879  eluz2b1  9954  uz2m1nn  9958  elnn0dc  9964  elnndc  9965  nn01to3  9970  zq  9979  nnrecq  9998  rpge0  10020  rpreccl  10034  mnflt  10138  pnfnlt  10142  mnfle  10147  xrlelttr  10161  xrltletr  10162  xrletr  10163  xgepnf  10171  xlt0neg2  10194  xle0neg2  10196  xaddpnf2  10202  xaddmnf2  10204  xaddid2  10218  elioomnf  10323  ige3m2fz  10406  fzshftral  10467  ige2m1fz1  10468  1fv  10498  4fvwrd4  10499  rebtwn2zlemstep  10639  qbtwnxr  10644  btwnzge0  10687  zmodid2  10741  q2txmodxeq0  10773  frec2uzrand  10794  frecuzrdgtcl  10801  frecfzennn  10815  nn0ennn  10822  uzennn  10825  0exp  10963  sqgt0api  11014  subsq2  11036  qsqeqor  11039  bernneq  11050  faclbnd  11131  faclbnd2  11132  faclbnd3  11133  hashinfuni  11168  hashxp  11219  hashpwfi  11221  iswrdiz  11259  lsw0  11300  ccatlid  11322  s1leng  11340  s1fv  11342  s111  11347  pfx0g  11396  2shfti  11544  reim  11565  imcl  11567  crim  11571  caucvgre  11694  rennim  11715  resqrexlemdecn  11725  qabsor  11788  absimle  11797  sqrtthi  11832  sqrtcli  11833  sqrtgt0i  11834  sqrtmsqi  11835  sqrtsqi  11836  sqsqrti  11837  sqrtge0i  11838  absidi  11839  absnidi  11840  xrmaxiflemlub  11961  serclim0  12018  fsum2d  12149  fsumcnv  12151  fsumconst  12168  modfsummodlem1  12170  fsumabs  12179  binom11  12200  prodf1  12256  prodfclim1  12258  prodsnf  12306  fprod2d  12337  fprodcnv  12339  efzval  12397  eftlub  12404  efsep  12405  ef4p  12408  efgt1  12411  reef11  12413  sinf  12418  cosf  12419  efi4p  12431  sinneg  12440  cosneg  12441  efival  12446  efmival  12447  cos01gt0  12477  sin02gt0  12478  absefib  12485  efieq1re  12486  demoivre  12487  demoivreALT  12488  eirraplem  12491  0dvds  12525  odd2np1lem  12586  odd2np1  12587  even2n  12588  mod2eq0even  12592  2teven  12601  opoe  12609  omoe  12610  opeo  12611  omeo  12612  m1exp1  12615  bits0e  12663  bits0o  12664  bitsinv1  12676  gcd0id  12703  gcdid0  12704  1gcd  12716  lcmdvds  12804  isprm2lem  12841  isprm3  12843  prmgt1  12857  coprm  12869  isevengcd2  12883  isoddgcd1  12884  sqpweven  12900  2sqpwodd  12901  pythagtriplem12  13001  pythagtriplem13  13002  pythagtriplem14  13003  pythagtriplem16  13005  pc2dvds  13056  oddprmdvds  13080  pockthi  13084  1arith2  13094  unennn  13235  ctinfomlemom  13265  qnnen  13269  ssnnctlemct  13284  strslfv  13344  strle1g  13406  1strbas  13417  tgval  13562  ismgmn0  13624  mulgval  13878  mulgfng  13880  mulg0  13881  mulg1  13885  mulg2  13887  isnsg  13958  ringidvalg  14207  issrg  14211  subrgpropd  14502  rrgval  14511  islmod  14568  scaffvalg  14583  islssm  14634  sraval  14714  mopnset  14829  metuex  14832  zrhval  14894  zrhvalg  14895  zrhex  14898  psrbag  14946  psrbagaddclfi  14954  istopon  15007  eltg4i  15049  eltg3  15051  tg1  15053  tg2  15054  topnex  15080  cldrcl  15096  restsn  15174  lmrcl  15186  metflem  15343  xmetf  15344  ismet2  15348  xmeteq0  15353  xmettri2  15355  xmetpsmet  15363  xmetres2  15373  blfvalps  15379  blex  15381  blvalps  15382  blval  15383  blfps  15403  blf  15404  mopnval  15436  cnbl0  15528  cnblcld  15529  blssioo  15547  resubmet  15550  cncfmet  15586  cnplimcim  15661  cnlimcim  15665  cnlimc  15666  dvfgg  15682  dvfpm  15683  dvfcnpm  15684  dvcj  15703  dvmptfsum  15719  reeff1olem  15765  ef2kpi  15800  sinperlem  15802  sin2kpi  15805  cos2kpi  15806  sinhalfpip  15814  sinhalfpim  15815  coshalfpip  15816  coshalfpim  15817  sincosq1sgn  15820  sinq12gt0  15824  sinkpi  15841  reeflog  15857  relogef  15858  logrpap0b  15870  loggt0b  15885  1cxp  15894  ecxp  15895  2logb9irrap  15971  0sgm  15982  lgsval2lem  16012  m1lgs  16087  1vgrex  16144  upgrfi  16226  umgredgnlp  16276  wlkop  16472  clwwlkn0  16532  djucllem  16711  bdrabexg  16815  bdunexb  16829  peano5set  16849  speano5  16853  bj-omtrans  16865  pw1ninf  16904  pwf1oexmid  16912  nninfsellemeq  16931  iswomninnlem  16973