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  1324  mp3an12  1327  mp3an13  1328  ax9o  1698  sbnfc2  3117  ssdifss  3265  undifss  3503  uneqdifeqim  3508  elssuni  3837  csbexa  4132  difexg  4144  rabexg  4146  abssexg  4182  snexg  4184  copsexg  4244  sotritric  4324  sotritrieq  4325  trsuc  4422  oneli  4428  unexb  4442  opeluu  4450  rabxfr  4470  reuhyp  4472  ordunisuc2r  4513  reg3exmid  4579  brrelex12i  4668  brrelex1i  4669  brrelex2i  4670  xpss2  4737  opabid2  4758  eliunxp  4766  releldmi  4866  relelrni  4867  dmexg  4891  rnexg  4892  elres  4943  resexg  4947  relbrcnvg  5007  brcodir  5016  sotri  5024  sotri2  5026  sotri3  5027  dfrel2  5079  coi1  5144  fco  5381  fssres  5391  fabexg  5403  fvopab3g  5589  mptrcl  5598  mpteqb  5606  elfvmptrab1  5610  ffvelcdmi  5650  fsn2  5690  dfmptg  5695  fvpr1  5720  fvconst2  5732  mptexg  5741  oprabid  5906  ovprc  5909  caovcl  6028  caovass  6034  caovdi  6053  elmpocl  6068  ofexg  6086  resfunexgALT  6108  fo1stresm  6161  fo2ndresm  6162  1stexg  6167  2ndexg  6168  elopabi  6195  mpoexxg  6210  mpoxopn0yelv  6239  rntpos  6257  smores  6292  tfr0dm  6322  tfrlemibxssdm  6327  tfrexlem  6334  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  rdgruledefgg  6375  rdgruledefg  6376  rdgivallem  6381  rdgexg  6389  frec0g  6397  ordgt0ge1  6435  omfnex  6449  oeiv  6456  nna0r  6478  nnm0r  6479  nnsucsssuc  6492  nn2m  6527  nnaordex  6528  nnawordex  6529  ecdmn0m  6576  ecelqsi  6588  ecidg  6598  ectocl  6601  encv  6745  f1oen  6758  ssdomg  6777  map1  6811  fiprc  6814  xpdom1  6834  fict  6867  isinfinf  6896  ac6sfi  6897  xpfi  6928  en1eqsn  6946  fidcenumlemr  6953  fiss  6975  eqinfti  7018  djueq2  7039  djulclr  7047  djurclr  7048  djulcl  7049  djurcl  7050  djuf1olem  7051  djulclb  7053  inl11  7063  eldju1st  7069  1stinl  7072  2ndinl  7073  1stinr  7074  2ndinr  7075  ctssdccl  7109  isomnimap  7134  ismkvmap  7151  iswomnimap  7163  djucomen  7214  exmidapne  7258  0nnq  7362  mulidnq  7387  archnqq  7415  prarloclemarch2  7417  nqnq0pi  7436  nq0m0r  7454  nq02m  7463  prarloclemlt  7491  prarloclemn  7497  prarloclem5  7498  addnqprllem  7525  addnqprulem  7526  appdivnq  7561  1idprl  7588  1idpru  7589  addextpr  7619  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprlemnbj  7665  caucvgprlemloc  7673  caucvgprprlemnbj  7691  caucvgprprlemloc  7701  caucvgprprlemaddq  7706  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemloc  7719  suplocexprlemlub  7722  0nsr  7747  ltsosr  7762  recexgt0sr  7771  prsrpos  7783  caucvgsr  7800  mappsrprg  7802  suplocsrlem  7806  mulresr  7836  axcnre  7879  axpre-ltwlin  7881  mullid  7954  0re  7956  axmulgt0  8028  ltnsym2  8047  eqlei  8050  ltnei  8060  muladd11  8089  cnegex  8134  0cnALT  8146  negcl  8156  negneg  8206  mul02  8343  mulm1  8356  lt0neg2  8425  le0neg2  8427  recexre  8534  recexgt0  8536  mulge0  8575  gt0ap0i  8583  recextlem1  8607  recexap  8609  recclapzi  8693  recap0apzi  8694  recidapzi  8695  divassapzi  8718  divmulapzi  8719  divdirapzi  8720  rerecclapzi  8732  ltp1  8800  recgt0i  8862  ltmul1i  8876  ltdiv1i  8877  ltmuldivi  8878  ltmul2i  8879  lemul1i  8880  lemul2i  8881  sup3exmid  8913  nngt1ne1  8953  nnrecre  8955  nn0ge0  9200  nn0addcl  9210  nn0mulcl  9211  zgt0ge1  9310  dfuzi  9362  eluzel2  9532  eluz2b1  9600  uz2m1nn  9604  elnn0dc  9610  elnndc  9611  nn01to3  9616  zq  9625  nnrecq  9644  rpge0  9665  rpreccl  9679  mnflt  9782  pnfnlt  9786  mnfle  9791  xrlelttr  9805  xrltletr  9806  xrletr  9807  xgepnf  9815  xlt0neg2  9838  xle0neg2  9840  xaddpnf2  9846  xaddmnf2  9848  xaddid2  9862  elioomnf  9967  ige3m2fz  10048  fzshftral  10107  ige2m1fz1  10108  1fv  10138  4fvwrd4  10139  rebtwn2zlemstep  10252  qbtwnxr  10257  btwnzge0  10299  zmodid2  10351  q2txmodxeq0  10383  frec2uzrand  10404  frecuzrdgtcl  10411  frecfzennn  10425  nn0ennn  10432  uzennn  10435  0exp  10554  sqgt0api  10605  subsq2  10627  qsqeqor  10630  bernneq  10640  faclbnd  10720  faclbnd2  10721  faclbnd3  10722  hashinfuni  10756  hashxp  10805  2shfti  10839  reim  10860  imcl  10862  crim  10866  caucvgre  10989  rennim  11010  resqrexlemdecn  11020  qabsor  11083  absimle  11092  sqrtthi  11127  sqrtcli  11128  sqrtgt0i  11129  sqrtmsqi  11130  sqrtsqi  11131  sqsqrti  11132  sqrtge0i  11133  absidi  11134  absnidi  11135  xrmaxiflemlub  11255  serclim0  11312  fsum2d  11442  fsumcnv  11444  fsumconst  11461  modfsummodlem1  11463  fsumabs  11472  binom11  11493  prodf1  11549  prodfclim1  11551  prodsnf  11599  fprod2d  11630  fprodcnv  11632  efzval  11690  eftlub  11697  efsep  11698  ef4p  11701  efgt1  11704  reef11  11706  sinf  11711  cosf  11712  efi4p  11724  sinneg  11733  cosneg  11734  efival  11739  efmival  11740  cos01gt0  11769  sin02gt0  11770  absefib  11777  efieq1re  11778  demoivre  11779  demoivreALT  11780  eirraplem  11783  0dvds  11817  odd2np1lem  11876  odd2np1  11877  even2n  11878  mod2eq0even  11882  2teven  11891  opoe  11899  omoe  11900  opeo  11901  omeo  11902  m1exp1  11905  gcd0id  11979  gcdid0  11980  1gcd  11992  lcmdvds  12078  isprm2lem  12115  isprm3  12117  prmgt1  12131  coprm  12143  isevengcd2  12157  isoddgcd1  12158  sqpweven  12174  2sqpwodd  12175  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem14  12276  pythagtriplem16  12278  pc2dvds  12328  oddprmdvds  12351  pockthi  12355  1arith2  12365  unennn  12397  ctinfomlemom  12427  qnnen  12431  ssnnctlemct  12446  strslfv  12506  strle1g  12564  1strbas  12575  tgval  12710  ismgmn0  12776  mulgval  12985  mulgfng  12986  mulg0  12987  mulg1  12989  mulg2  12991  isnsg  13060  ringidvalg  13142  issrg  13146  subrgpropd  13367  islmod  13379  scaffvalg  13394  istopon  13483  eltg4i  13525  eltg3  13527  tg1  13529  tg2  13530  topnex  13556  cldrcl  13572  restsn  13650  lmrcl  13661  metflem  13819  xmetf  13820  ismet2  13824  xmeteq0  13829  xmettri2  13831  xmetpsmet  13839  xmetres2  13849  blfvalps  13855  blex  13857  blvalps  13858  blval  13859  blfps  13879  blf  13880  mopnval  13912  cnbl0  14004  cnblcld  14005  blssioo  14015  resubmet  14018  cncfmet  14049  cnplimcim  14106  cnlimcim  14110  cnlimc  14111  dvfgg  14127  dvfpm  14128  dvfcnpm  14129  dvcj  14143  reeff1olem  14162  ef2kpi  14197  sinperlem  14199  sin2kpi  14202  cos2kpi  14203  sinhalfpip  14211  sinhalfpim  14212  coshalfpip  14213  coshalfpim  14214  sincosq1sgn  14217  sinq12gt0  14221  sinkpi  14238  reeflog  14254  relogef  14255  logrpap0b  14267  loggt0b  14282  1cxp  14291  ecxp  14292  2logb9irrap  14365  lgsval2lem  14381  m1lgs  14422  djucllem  14522  bdrabexg  14628  bdunexb  14642  peano5set  14662  speano5  14666  bj-omtrans  14678  pwf1oexmid  14719  nninfsellemeq  14733  iswomninnlem  14767