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  3595  uneqdifeqim  3600  elssuni  3948  csbexa  4245  difexg  4258  rabexg  4261  abssexg  4301  snexg  4303  copsexg  4366  sotritric  4451  sotritrieq  4452  trsuc  4549  oneli  4555  unexb  4569  opeluu  4577  rabxfr  4597  reuhyp  4599  ordunisuc2r  4642  reg3exmid  4708  brrelex12i  4798  brrelex1i  4799  brrelex2i  4800  xpss2  4867  opabid2  4892  eliunxp  4900  releldmi  5002  relelrni  5003  dmexg  5027  rnexg  5028  elres  5080  resexg  5084  relbrcnvg  5147  brcodir  5156  sotri  5164  sotri2  5166  sotri3  5167  dfrel2  5219  coi1  5284  fco  5533  fssres  5546  fabexg  5560  fvopab3g  5756  mptrcl  5766  mpteqb  5774  elfvmptrab1  5778  ffvelcdmi  5817  fsn2  5857  dfmptg  5863  fcof  5869  fvpr1  5894  fvconst2  5906  mptexg  5917  oprabid  6091  ovprc  6095  caovcl  6218  caovass  6224  caovdi  6243  elmpocl  6258  relmptopab  6265  ofexg  6281  resfunexgALT  6311  fo1stresm  6369  fo2ndresm  6370  1stexg  6375  2ndexg  6376  elopabi  6405  mpoexxg  6420  elmpom  6448  supp0  6452  mpoxopn0yelv  6484  rntpos  6502  smores  6537  tfr0dm  6567  tfrlemibxssdm  6572  tfrexlem  6579  tfr1onlembxssdm  6588  tfrcllembxssdm  6601  rdgruledefgg  6620  rdgruledefg  6621  rdgivallem  6626  rdgexg  6634  frec0g  6642  ordgt0ge1  6682  omfnex  6696  oeiv  6703  nna0r  6725  nnm0r  6726  nnsucsssuc  6739  nn2m  6774  nnaordex  6775  nnawordex  6776  ecdmn0m  6825  ecelqsi  6837  ecidg  6847  ectocl  6850  encv  6995  f1oen  7012  ssdomg  7032  map1  7068  fiprc  7071  dom1o  7083  xpdom1  7100  fict  7137  isinfinf  7168  ac6sfi  7169  xpfi  7206  en1eqsn  7232  fidcenumlemr  7239  fiss  7278  fipwfi  7286  eqinfti  7325  djueq2  7346  djulclr  7354  djurclr  7355  djulcl  7356  djurcl  7357  djuf1olem  7358  djulclb  7360  inl11  7370  eldju1st  7376  1stinl  7379  2ndinl  7380  1stinr  7381  2ndinr  7382  ctssdccl  7416  isomnimap  7442  ismkvmap  7459  iswomnimap  7471  finacn  7525  djucomen  7537  exmidapne  7591  0nnq  7696  mulidnq  7721  archnqq  7749  prarloclemarch2  7751  nqnq0pi  7770  nq0m0r  7788  nq02m  7797  prarloclemlt  7825  prarloclemn  7831  prarloclem5  7832  addnqprllem  7859  addnqprulem  7860  appdivnq  7895  1idprl  7922  1idpru  7923  addextpr  7953  cauappcvgprlemdisj  7983  cauappcvgprlemloc  7984  cauappcvgprlemladdru  7988  cauappcvgprlemladdrl  7989  caucvgprlemnbj  7999  caucvgprlemloc  8007  caucvgprprlemnbj  8025  caucvgprprlemloc  8035  caucvgprprlemaddq  8040  suplocexprlemmu  8050  suplocexprlemru  8051  suplocexprlemloc  8053  suplocexprlemlub  8056  0nsr  8081  ltsosr  8096  recexgt0sr  8105  prsrpos  8117  caucvgsr  8134  mappsrprg  8136  suplocsrlem  8140  mulresr  8170  axcnre  8213  axpre-ltwlin  8215  mullid  8289  0re  8291  axmulgt0  8362  ltnsym2  8381  eqlei  8384  ltnei  8394  muladd11  8424  cnegex  8469  0cnALT  8481  negcl  8491  negneg  8541  mul02  8679  mulm1  8692  lt0neg2  8762  le0neg2  8764  recexre  8871  recexgt0  8873  mulge0  8912  gt0ap0i  8920  recextlem1  8944  recexap  8946  recclapzi  9032  recap0apzi  9033  recidapzi  9034  divassapzi  9057  divmulapzi  9058  divdirapzi  9059  rerecclapzi  9071  ltp1  9139  recgt0i  9201  ltmul1i  9215  ltdiv1i  9216  ltmuldivi  9217  ltmul2i  9218  lemul1i  9219  lemul2i  9220  sup3exmid  9252  nngt1ne1  9293  nnrecre  9295  nn0ge0  9542  nn0addcl  9552  nn0mulcl  9553  zgt0ge1  9657  dfuzi  9710  eluzel2  9880  eluz2b1  9955  uz2m1nn  9959  elnn0dc  9965  elnndc  9966  nn01to3  9971  zq  9980  nnrecq  9999  rpge0  10021  rpreccl  10035  mnflt  10139  pnfnlt  10143  mnfle  10148  xrlelttr  10162  xrltletr  10163  xrletr  10164  xgepnf  10172  xlt0neg2  10195  xle0neg2  10197  xaddpnf2  10203  xaddmnf2  10205  xaddid2  10219  elioomnf  10324  ige3m2fz  10407  fzshftral  10468  ige2m1fz1  10469  1fv  10499  4fvwrd4  10500  rebtwn2zlemstep  10640  qbtwnxr  10645  btwnzge0  10688  zmodid2  10742  q2txmodxeq0  10774  frec2uzrand  10795  frecuzrdgtcl  10802  frecfzennn  10816  nn0ennn  10823  uzennn  10826  0exp  10964  sqgt0api  11015  subsq2  11037  qsqeqor  11040  bernneq  11051  faclbnd  11132  faclbnd2  11133  faclbnd3  11134  hashinfuni  11169  hashxp  11220  hashpwfi  11222  iswrdiz  11260  lsw0  11301  ccatlid  11323  s1leng  11341  s1fv  11343  s111  11348  pfx0g  11397  2shfti  11545  reim  11566  imcl  11568  crim  11572  caucvgre  11696  rennim  11717  resqrexlemdecn  11727  qabsor  11790  absimle  11799  sqrtthi  11834  sqrtcli  11835  sqrtgt0i  11836  sqrtmsqi  11837  sqrtsqi  11838  sqsqrti  11839  sqrtge0i  11840  absidi  11841  absnidi  11842  xrmaxiflemlub  11963  serclim0  12020  fsum2d  12151  fsumcnv  12153  fsumconst  12170  modfsummodlem1  12172  fsumabs  12181  binom11  12202  prodf1  12258  prodfclim1  12260  prodsnf  12308  fprod2d  12339  fprodcnv  12341  efzval  12399  eftlub  12406  efsep  12407  ef4p  12410  efgt1  12413  reef11  12415  sinf  12420  cosf  12421  efi4p  12433  sinneg  12442  cosneg  12443  efival  12448  efmival  12449  cos01gt0  12479  sin02gt0  12480  absefib  12487  efieq1re  12488  demoivre  12489  demoivreALT  12490  eirraplem  12493  0dvds  12527  odd2np1lem  12588  odd2np1  12589  even2n  12590  mod2eq0even  12594  2teven  12603  opoe  12611  omoe  12612  opeo  12613  omeo  12614  m1exp1  12617  bits0e  12665  bits0o  12666  bitsinv1  12678  gcd0id  12705  gcdid0  12706  1gcd  12718  lcmdvds  12806  isprm2lem  12843  isprm3  12845  prmgt1  12859  coprm  12871  isevengcd2  12885  isoddgcd1  12886  sqpweven  12902  2sqpwodd  12903  pythagtriplem12  13003  pythagtriplem13  13004  pythagtriplem14  13005  pythagtriplem16  13007  pc2dvds  13058  oddprmdvds  13082  pockthi  13086  1arith2  13096  unennn  13237  ctinfomlemom  13267  qnnen  13271  ssnnctlemct  13286  strslfv  13346  strle1g  13408  1strbas  13419  tgval  13564  ismgmn0  13626  mulgval  13880  mulgfng  13882  mulg0  13883  mulg1  13887  mulg2  13889  isnsg  13960  ringidvalg  14209  issrg  14213  subrgpropd  14504  rrgval  14513  islmod  14570  scaffvalg  14585  islssm  14636  sraval  14716  mopnset  14831  metuex  14834  zrhval  14896  zrhvalg  14897  zrhex  14900  psrbag  14948  psrbagaddclfi  14956  istopon  15009  eltg4i  15051  eltg3  15053  tg1  15055  tg2  15056  topnex  15082  cldrcl  15098  restsn  15176  lmrcl  15188  metflem  15345  xmetf  15346  ismet2  15350  xmeteq0  15355  xmettri2  15357  xmetpsmet  15365  xmetres2  15375  blfvalps  15381  blex  15383  blvalps  15384  blval  15385  blfps  15405  blf  15406  mopnval  15438  cnbl0  15530  cnblcld  15531  blssioo  15549  resubmet  15552  cncfmet  15588  cnplimcim  15663  cnlimcim  15667  cnlimc  15668  dvfgg  15684  dvfpm  15685  dvfcnpm  15686  dvcj  15705  dvmptfsum  15721  reeff1olem  15767  ef2kpi  15802  sinperlem  15804  sin2kpi  15807  cos2kpi  15808  sinhalfpip  15816  sinhalfpim  15817  coshalfpip  15818  coshalfpim  15819  sincosq1sgn  15822  sinq12gt0  15826  sinkpi  15843  reeflog  15859  relogef  15860  logrpap0b  15872  loggt0b  15887  1cxp  15896  ecxp  15897  2logb9irrap  15973  0sgm  15984  lgsval2lem  16014  m1lgs  16089  1vgrex  16146  upgrfi  16228  umgredgnlp  16278  wlkop  16474  clwwlkn0  16534  djucllem  16713  bdrabexg  16817  bdunexb  16831  peano5set  16851  speano5  16855  bj-omtrans  16867  pw1ninf  16906  pwf1oexmid  16914  nninfsellemeq  16933  iswomninnlem  16975