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  3198  ssdifss  3348  undifss  3589  uneqdifeqim  3594  elssuni  3941  csbexa  4238  difexg  4251  rabexg  4254  abssexg  4294  snexg  4296  copsexg  4359  sotritric  4444  sotritrieq  4445  trsuc  4542  oneli  4548  unexb  4562  opeluu  4570  rabxfr  4590  reuhyp  4592  ordunisuc2r  4635  reg3exmid  4701  brrelex12i  4791  brrelex1i  4792  brrelex2i  4793  xpss2  4860  opabid2  4885  eliunxp  4893  releldmi  4995  relelrni  4996  dmexg  5020  rnexg  5021  elres  5073  resexg  5077  relbrcnvg  5140  brcodir  5149  sotri  5157  sotri2  5159  sotri3  5160  dfrel2  5212  coi1  5277  fco  5526  fssres  5539  fabexg  5553  fvopab3g  5749  mptrcl  5759  mpteqb  5767  elfvmptrab1  5771  ffvelcdmi  5810  fsn2  5850  dfmptg  5856  fcof  5862  fvpr1  5887  fvconst2  5899  mptexg  5910  oprabid  6081  ovprc  6085  caovcl  6208  caovass  6214  caovdi  6233  elmpocl  6248  relmptopab  6255  ofexg  6270  resfunexgALT  6300  fo1stresm  6354  fo2ndresm  6355  1stexg  6360  2ndexg  6361  elopabi  6390  mpoexxg  6405  elmpom  6433  supp0  6437  mpoxopn0yelv  6469  rntpos  6487  smores  6522  tfr0dm  6552  tfrlemibxssdm  6557  tfrexlem  6564  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  rdgruledefgg  6605  rdgruledefg  6606  rdgivallem  6611  rdgexg  6619  frec0g  6627  ordgt0ge1  6667  omfnex  6681  oeiv  6688  nna0r  6710  nnm0r  6711  nnsucsssuc  6724  nn2m  6759  nnaordex  6760  nnawordex  6761  ecdmn0m  6810  ecelqsi  6822  ecidg  6832  ectocl  6835  encv  6980  f1oen  6997  ssdomg  7017  map1  7053  fiprc  7056  dom1o  7068  xpdom1  7085  fict  7122  isinfinf  7153  ac6sfi  7154  xpfi  7191  en1eqsn  7217  fidcenumlemr  7224  fiss  7263  fipwfi  7271  eqinfti  7310  djueq2  7331  djulclr  7339  djurclr  7340  djulcl  7341  djurcl  7342  djuf1olem  7343  djulclb  7345  inl11  7355  eldju1st  7361  1stinl  7364  2ndinl  7365  1stinr  7366  2ndinr  7367  ctssdccl  7401  isomnimap  7427  ismkvmap  7444  iswomnimap  7456  finacn  7510  djucomen  7522  exmidapne  7570  0nnq  7675  mulidnq  7700  archnqq  7728  prarloclemarch2  7730  nqnq0pi  7749  nq0m0r  7767  nq02m  7776  prarloclemlt  7804  prarloclemn  7810  prarloclem5  7811  addnqprllem  7838  addnqprulem  7839  appdivnq  7874  1idprl  7901  1idpru  7902  addextpr  7932  cauappcvgprlemdisj  7962  cauappcvgprlemloc  7963  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  caucvgprlemnbj  7978  caucvgprlemloc  7986  caucvgprprlemnbj  8004  caucvgprprlemloc  8014  caucvgprprlemaddq  8019  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemloc  8032  suplocexprlemlub  8035  0nsr  8060  ltsosr  8075  recexgt0sr  8084  prsrpos  8096  caucvgsr  8113  mappsrprg  8115  suplocsrlem  8119  mulresr  8149  axcnre  8192  axpre-ltwlin  8194  mullid  8268  0re  8270  axmulgt0  8341  ltnsym2  8360  eqlei  8363  ltnei  8373  muladd11  8402  cnegex  8447  0cnALT  8459  negcl  8469  negneg  8519  mul02  8656  mulm1  8669  lt0neg2  8739  le0neg2  8741  recexre  8848  recexgt0  8850  mulge0  8889  gt0ap0i  8897  recextlem1  8921  recexap  8923  recclapzi  9007  recap0apzi  9008  recidapzi  9009  divassapzi  9032  divmulapzi  9033  divdirapzi  9034  rerecclapzi  9046  ltp1  9114  recgt0i  9176  ltmul1i  9190  ltdiv1i  9191  ltmuldivi  9192  ltmul2i  9193  lemul1i  9194  lemul2i  9195  sup3exmid  9227  nngt1ne1  9268  nnrecre  9270  nn0ge0  9517  nn0addcl  9527  nn0mulcl  9528  zgt0ge1  9632  dfuzi  9684  eluzel2  9854  eluz2b1  9929  uz2m1nn  9933  elnn0dc  9939  elnndc  9940  nn01to3  9945  zq  9954  nnrecq  9973  rpge0  9995  rpreccl  10009  mnflt  10112  pnfnlt  10116  mnfle  10121  xrlelttr  10135  xrltletr  10136  xrletr  10137  xgepnf  10145  xlt0neg2  10168  xle0neg2  10170  xaddpnf2  10176  xaddmnf2  10178  xaddid2  10192  elioomnf  10297  ige3m2fz  10379  fzshftral  10438  ige2m1fz1  10439  1fv  10469  4fvwrd4  10470  rebtwn2zlemstep  10608  qbtwnxr  10613  btwnzge0  10656  zmodid2  10710  q2txmodxeq0  10742  frec2uzrand  10763  frecuzrdgtcl  10770  frecfzennn  10784  nn0ennn  10791  uzennn  10794  0exp  10932  sqgt0api  10983  subsq2  11005  qsqeqor  11008  bernneq  11018  faclbnd  11099  faclbnd2  11100  faclbnd3  11101  hashinfuni  11135  hashxp  11186  iswrdiz  11224  lsw0  11265  ccatlid  11287  s1leng  11305  s1fv  11307  s111  11312  pfx0g  11361  2shfti  11509  reim  11530  imcl  11532  crim  11536  caucvgre  11659  rennim  11680  resqrexlemdecn  11690  qabsor  11753  absimle  11762  sqrtthi  11797  sqrtcli  11798  sqrtgt0i  11799  sqrtmsqi  11800  sqrtsqi  11801  sqsqrti  11802  sqrtge0i  11803  absidi  11804  absnidi  11805  xrmaxiflemlub  11926  serclim0  11983  fsum2d  12114  fsumcnv  12116  fsumconst  12133  modfsummodlem1  12135  fsumabs  12144  binom11  12165  prodf1  12221  prodfclim1  12223  prodsnf  12271  fprod2d  12302  fprodcnv  12304  efzval  12362  eftlub  12369  efsep  12370  ef4p  12373  efgt1  12376  reef11  12378  sinf  12383  cosf  12384  efi4p  12396  sinneg  12405  cosneg  12406  efival  12411  efmival  12412  cos01gt0  12442  sin02gt0  12443  absefib  12450  efieq1re  12451  demoivre  12452  demoivreALT  12453  eirraplem  12456  0dvds  12490  odd2np1lem  12551  odd2np1  12552  even2n  12553  mod2eq0even  12557  2teven  12566  opoe  12574  omoe  12575  opeo  12576  omeo  12577  m1exp1  12580  bits0e  12628  bits0o  12629  bitsinv1  12641  gcd0id  12668  gcdid0  12669  1gcd  12681  lcmdvds  12769  isprm2lem  12806  isprm3  12808  prmgt1  12822  coprm  12834  isevengcd2  12848  isoddgcd1  12849  sqpweven  12865  2sqpwodd  12866  pythagtriplem12  12966  pythagtriplem13  12967  pythagtriplem14  12968  pythagtriplem16  12970  pc2dvds  13021  oddprmdvds  13045  pockthi  13049  1arith2  13059  unennn  13137  ctinfomlemom  13167  qnnen  13171  ssnnctlemct  13186  strslfv  13246  strle1g  13308  1strbas  13319  tgval  13464  ismgmn0  13560  mulgval  13828  mulgfng  13830  mulg0  13831  mulg1  13835  mulg2  13837  isnsg  13908  ringidvalg  14094  issrg  14098  subrgpropd  14387  rrgval  14396  islmod  14426  scaffvalg  14441  islssm  14492  sraval  14572  mopnset  14687  metuex  14690  zrhval  14752  zrhvalg  14753  zrhex  14756  psrbag  14804  psrbagaddclfi  14812  istopon  14865  eltg4i  14907  eltg3  14909  tg1  14911  tg2  14912  topnex  14938  cldrcl  14954  restsn  15032  lmrcl  15044  metflem  15201  xmetf  15202  ismet2  15206  xmeteq0  15211  xmettri2  15213  xmetpsmet  15221  xmetres2  15231  blfvalps  15237  blex  15239  blvalps  15240  blval  15241  blfps  15261  blf  15262  mopnval  15294  cnbl0  15386  cnblcld  15387  blssioo  15405  resubmet  15408  cncfmet  15444  cnplimcim  15519  cnlimcim  15523  cnlimc  15524  dvfgg  15540  dvfpm  15541  dvfcnpm  15542  dvcj  15561  dvmptfsum  15577  reeff1olem  15623  ef2kpi  15658  sinperlem  15660  sin2kpi  15663  cos2kpi  15664  sinhalfpip  15672  sinhalfpim  15673  coshalfpip  15674  coshalfpim  15675  sincosq1sgn  15678  sinq12gt0  15682  sinkpi  15699  reeflog  15715  relogef  15716  logrpap0b  15728  loggt0b  15743  1cxp  15752  ecxp  15753  2logb9irrap  15829  0sgm  15840  lgsval2lem  15870  m1lgs  15945  1vgrex  16002  upgrfi  16084  umgredgnlp  16134  wlkop  16330  clwwlkn0  16390  djucllem  16559  bdrabexg  16663  bdunexb  16677  peano5set  16697  speano5  16701  bj-omtrans  16713  pw1ninf  16752  pwf1oexmid  16760  nninfsellemeq  16779  iswomninnlem  16821