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  1339  mp3an12  1342  mp3an13  1343  ax9o  1724  sbnfc2  3165  ssdifss  3314  undifss  3552  uneqdifeqim  3557  elssuni  3895  csbexa  4192  difexg  4204  rabexg  4206  abssexg  4245  snexg  4247  copsexg  4309  sotritric  4392  sotritrieq  4393  trsuc  4490  oneli  4496  unexb  4510  opeluu  4518  rabxfr  4538  reuhyp  4540  ordunisuc2r  4583  reg3exmid  4649  brrelex12i  4738  brrelex1i  4739  brrelex2i  4740  xpss2  4807  opabid2  4830  eliunxp  4838  releldmi  4939  relelrni  4940  dmexg  4964  rnexg  4965  elres  5017  resexg  5021  relbrcnvg  5083  brcodir  5092  sotri  5100  sotri2  5102  sotri3  5103  dfrel2  5155  coi1  5220  fco  5465  fssres  5477  fabexg  5489  fvopab3g  5680  mptrcl  5690  mpteqb  5698  elfvmptrab1  5702  ffvelcdmi  5742  fsn2  5782  dfmptg  5787  fvpr1  5816  fvconst2  5828  mptexg  5837  oprabid  6006  ovprc  6010  caovcl  6131  caovass  6137  caovdi  6156  elmpocl  6171  ofexg  6193  resfunexgALT  6223  fo1stresm  6277  fo2ndresm  6278  1stexg  6283  2ndexg  6284  elopabi  6311  mpoexxg  6326  mpoxopn0yelv  6355  rntpos  6373  smores  6408  tfr0dm  6438  tfrlemibxssdm  6443  tfrexlem  6450  tfr1onlembxssdm  6459  tfrcllembxssdm  6472  rdgruledefgg  6491  rdgruledefg  6492  rdgivallem  6497  rdgexg  6505  frec0g  6513  ordgt0ge1  6551  omfnex  6565  oeiv  6572  nna0r  6594  nnm0r  6595  nnsucsssuc  6608  nn2m  6643  nnaordex  6644  nnawordex  6645  ecdmn0m  6694  ecelqsi  6706  ecidg  6716  ectocl  6719  encv  6863  f1oen  6880  ssdomg  6900  map1  6935  fiprc  6938  xpdom1  6962  fict  6998  isinfinf  7027  ac6sfi  7028  xpfi  7062  en1eqsn  7083  fidcenumlemr  7090  fiss  7112  eqinfti  7155  djueq2  7176  djulclr  7184  djurclr  7185  djulcl  7186  djurcl  7187  djuf1olem  7188  djulclb  7190  inl11  7200  eldju1st  7206  1stinl  7209  2ndinl  7210  1stinr  7211  2ndinr  7212  ctssdccl  7246  isomnimap  7272  ismkvmap  7289  iswomnimap  7301  finacn  7354  djucomen  7366  exmidapne  7414  0nnq  7519  mulidnq  7544  archnqq  7572  prarloclemarch2  7574  nqnq0pi  7593  nq0m0r  7611  nq02m  7620  prarloclemlt  7648  prarloclemn  7654  prarloclem5  7655  addnqprllem  7682  addnqprulem  7683  appdivnq  7718  1idprl  7745  1idpru  7746  addextpr  7776  cauappcvgprlemdisj  7806  cauappcvgprlemloc  7807  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  caucvgprlemnbj  7822  caucvgprlemloc  7830  caucvgprprlemnbj  7848  caucvgprprlemloc  7858  caucvgprprlemaddq  7863  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemloc  7876  suplocexprlemlub  7879  0nsr  7904  ltsosr  7919  recexgt0sr  7928  prsrpos  7940  caucvgsr  7957  mappsrprg  7959  suplocsrlem  7963  mulresr  7993  axcnre  8036  axpre-ltwlin  8038  mullid  8112  0re  8114  axmulgt0  8186  ltnsym2  8205  eqlei  8208  ltnei  8218  muladd11  8247  cnegex  8292  0cnALT  8304  negcl  8314  negneg  8364  mul02  8501  mulm1  8514  lt0neg2  8584  le0neg2  8586  recexre  8693  recexgt0  8695  mulge0  8734  gt0ap0i  8742  recextlem1  8766  recexap  8768  recclapzi  8852  recap0apzi  8853  recidapzi  8854  divassapzi  8877  divmulapzi  8878  divdirapzi  8879  rerecclapzi  8891  ltp1  8959  recgt0i  9021  ltmul1i  9035  ltdiv1i  9036  ltmuldivi  9037  ltmul2i  9038  lemul1i  9039  lemul2i  9040  sup3exmid  9072  nngt1ne1  9113  nnrecre  9115  nn0ge0  9362  nn0addcl  9372  nn0mulcl  9373  zgt0ge1  9473  dfuzi  9525  eluzel2  9695  eluz2b1  9764  uz2m1nn  9768  elnn0dc  9774  elnndc  9775  nn01to3  9780  zq  9789  nnrecq  9808  rpge0  9830  rpreccl  9844  mnflt  9947  pnfnlt  9951  mnfle  9956  xrlelttr  9970  xrltletr  9971  xrletr  9972  xgepnf  9980  xlt0neg2  10003  xle0neg2  10005  xaddpnf2  10011  xaddmnf2  10013  xaddid2  10027  elioomnf  10132  ige3m2fz  10213  fzshftral  10272  ige2m1fz1  10273  1fv  10303  4fvwrd4  10304  rebtwn2zlemstep  10439  qbtwnxr  10444  btwnzge0  10487  zmodid2  10541  q2txmodxeq0  10573  frec2uzrand  10594  frecuzrdgtcl  10601  frecfzennn  10615  nn0ennn  10622  uzennn  10625  0exp  10763  sqgt0api  10814  subsq2  10836  qsqeqor  10839  bernneq  10849  faclbnd  10930  faclbnd2  10931  faclbnd3  10932  hashinfuni  10966  hashxp  11015  iswrdiz  11045  lsw0  11085  ccatlid  11107  s1leng  11123  s1fv  11125  s111  11130  pfx0g  11174  2shfti  11308  reim  11329  imcl  11331  crim  11335  caucvgre  11458  rennim  11479  resqrexlemdecn  11489  qabsor  11552  absimle  11561  sqrtthi  11596  sqrtcli  11597  sqrtgt0i  11598  sqrtmsqi  11599  sqrtsqi  11600  sqsqrti  11601  sqrtge0i  11602  absidi  11603  absnidi  11604  xrmaxiflemlub  11725  serclim0  11782  fsum2d  11912  fsumcnv  11914  fsumconst  11931  modfsummodlem1  11933  fsumabs  11942  binom11  11963  prodf1  12019  prodfclim1  12021  prodsnf  12069  fprod2d  12100  fprodcnv  12102  efzval  12160  eftlub  12167  efsep  12168  ef4p  12171  efgt1  12174  reef11  12176  sinf  12181  cosf  12182  efi4p  12194  sinneg  12203  cosneg  12204  efival  12209  efmival  12210  cos01gt0  12240  sin02gt0  12241  absefib  12248  efieq1re  12249  demoivre  12250  demoivreALT  12251  eirraplem  12254  0dvds  12288  odd2np1lem  12349  odd2np1  12350  even2n  12351  mod2eq0even  12355  2teven  12364  opoe  12372  omoe  12373  opeo  12374  omeo  12375  m1exp1  12378  bits0e  12426  bits0o  12427  bitsinv1  12439  gcd0id  12466  gcdid0  12467  1gcd  12479  lcmdvds  12567  isprm2lem  12604  isprm3  12606  prmgt1  12620  coprm  12632  isevengcd2  12646  isoddgcd1  12647  sqpweven  12663  2sqpwodd  12664  pythagtriplem12  12764  pythagtriplem13  12765  pythagtriplem14  12766  pythagtriplem16  12768  pc2dvds  12819  oddprmdvds  12843  pockthi  12847  1arith2  12857  unennn  12934  ctinfomlemom  12964  qnnen  12968  ssnnctlemct  12983  strslfv  13043  strle1g  13105  1strbas  13116  tgval  13261  ismgmn0  13357  mulgval  13625  mulgfng  13627  mulg0  13628  mulg1  13632  mulg2  13634  isnsg  13705  ringidvalg  13890  issrg  13894  subrgpropd  14182  rrgval  14191  islmod  14220  scaffvalg  14235  islssm  14286  sraval  14366  mopnset  14481  metuex  14484  zrhval  14546  zrhvalg  14547  zrhex  14550  psrbag  14598  istopon  14652  eltg4i  14694  eltg3  14696  tg1  14698  tg2  14699  topnex  14725  cldrcl  14741  restsn  14819  lmrcl  14830  metflem  14988  xmetf  14989  ismet2  14993  xmeteq0  14998  xmettri2  15000  xmetpsmet  15008  xmetres2  15018  blfvalps  15024  blex  15026  blvalps  15027  blval  15028  blfps  15048  blf  15049  mopnval  15081  cnbl0  15173  cnblcld  15174  blssioo  15192  resubmet  15195  cncfmet  15231  cnplimcim  15306  cnlimcim  15310  cnlimc  15311  dvfgg  15327  dvfpm  15328  dvfcnpm  15329  dvcj  15348  dvmptfsum  15364  reeff1olem  15410  ef2kpi  15445  sinperlem  15447  sin2kpi  15450  cos2kpi  15451  sinhalfpip  15459  sinhalfpim  15460  coshalfpip  15461  coshalfpim  15462  sincosq1sgn  15465  sinq12gt0  15469  sinkpi  15486  reeflog  15502  relogef  15503  logrpap0b  15515  loggt0b  15530  1cxp  15539  ecxp  15540  2logb9irrap  15616  0sgm  15624  lgsval2lem  15654  m1lgs  15729  1vgrex  15786  upgrfi  15867  umgredgnlp  15915  djucllem  16074  bdrabexg  16179  bdunexb  16193  peano5set  16213  speano5  16217  bj-omtrans  16229  dom1o  16266  pwf1oexmid  16276  nninfsellemeq  16291  iswomninnlem  16328