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  1358  mp3an12  1361  mp3an13  1362  ax9o  1744  sbnfc2  3186  ssdifss  3335  undifss  3573  uneqdifeqim  3578  elssuni  3919  csbexa  4216  difexg  4229  rabexg  4231  abssexg  4270  snexg  4272  copsexg  4334  sotritric  4419  sotritrieq  4420  trsuc  4517  oneli  4523  unexb  4537  opeluu  4545  rabxfr  4565  reuhyp  4567  ordunisuc2r  4610  reg3exmid  4676  brrelex12i  4766  brrelex1i  4767  brrelex2i  4768  xpss2  4835  opabid2  4859  eliunxp  4867  releldmi  4969  relelrni  4970  dmexg  4994  rnexg  4995  elres  5047  resexg  5051  relbrcnvg  5113  brcodir  5122  sotri  5130  sotri2  5132  sotri3  5133  dfrel2  5185  coi1  5250  fco  5497  fssres  5509  fabexg  5521  fvopab3g  5715  mptrcl  5725  mpteqb  5733  elfvmptrab1  5737  ffvelcdmi  5777  fsn2  5817  dfmptg  5822  fcof  5828  fvpr1  5853  fvconst2  5865  mptexg  5874  oprabid  6045  ovprc  6049  caovcl  6172  caovass  6178  caovdi  6197  elmpocl  6212  relmptopab  6219  ofexg  6235  resfunexgALT  6265  fo1stresm  6319  fo2ndresm  6320  1stexg  6325  2ndexg  6326  elopabi  6355  mpoexxg  6370  elmpom  6398  mpoxopn0yelv  6400  rntpos  6418  smores  6453  tfr0dm  6483  tfrlemibxssdm  6488  tfrexlem  6495  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  rdgruledefgg  6536  rdgruledefg  6537  rdgivallem  6542  rdgexg  6550  frec0g  6558  ordgt0ge1  6598  omfnex  6612  oeiv  6619  nna0r  6641  nnm0r  6642  nnsucsssuc  6655  nn2m  6690  nnaordex  6691  nnawordex  6692  ecdmn0m  6741  ecelqsi  6753  ecidg  6763  ectocl  6766  encv  6910  f1oen  6927  ssdomg  6947  map1  6982  fiprc  6985  dom1o  6997  xpdom1  7014  fict  7050  isinfinf  7081  ac6sfi  7082  xpfi  7119  en1eqsn  7141  fidcenumlemr  7148  fiss  7170  eqinfti  7213  djueq2  7234  djulclr  7242  djurclr  7243  djulcl  7244  djurcl  7245  djuf1olem  7246  djulclb  7248  inl11  7258  eldju1st  7264  1stinl  7267  2ndinl  7268  1stinr  7269  2ndinr  7270  ctssdccl  7304  isomnimap  7330  ismkvmap  7347  iswomnimap  7359  finacn  7412  djucomen  7424  exmidapne  7472  0nnq  7577  mulidnq  7602  archnqq  7630  prarloclemarch2  7632  nqnq0pi  7651  nq0m0r  7669  nq02m  7678  prarloclemlt  7706  prarloclemn  7712  prarloclem5  7713  addnqprllem  7740  addnqprulem  7741  appdivnq  7776  1idprl  7803  1idpru  7804  addextpr  7834  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemnbj  7880  caucvgprlemloc  7888  caucvgprprlemnbj  7906  caucvgprprlemloc  7916  caucvgprprlemaddq  7921  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemloc  7934  suplocexprlemlub  7937  0nsr  7962  ltsosr  7977  recexgt0sr  7986  prsrpos  7998  caucvgsr  8015  mappsrprg  8017  suplocsrlem  8021  mulresr  8051  axcnre  8094  axpre-ltwlin  8096  mullid  8170  0re  8172  axmulgt0  8244  ltnsym2  8263  eqlei  8266  ltnei  8276  muladd11  8305  cnegex  8350  0cnALT  8362  negcl  8372  negneg  8422  mul02  8559  mulm1  8572  lt0neg2  8642  le0neg2  8644  recexre  8751  recexgt0  8753  mulge0  8792  gt0ap0i  8800  recextlem1  8824  recexap  8826  recclapzi  8910  recap0apzi  8911  recidapzi  8912  divassapzi  8935  divmulapzi  8936  divdirapzi  8937  rerecclapzi  8949  ltp1  9017  recgt0i  9079  ltmul1i  9093  ltdiv1i  9094  ltmuldivi  9095  ltmul2i  9096  lemul1i  9097  lemul2i  9098  sup3exmid  9130  nngt1ne1  9171  nnrecre  9173  nn0ge0  9420  nn0addcl  9430  nn0mulcl  9431  zgt0ge1  9531  dfuzi  9583  eluzel2  9753  eluz2b1  9828  uz2m1nn  9832  elnn0dc  9838  elnndc  9839  nn01to3  9844  zq  9853  nnrecq  9872  rpge0  9894  rpreccl  9908  mnflt  10011  pnfnlt  10015  mnfle  10020  xrlelttr  10034  xrltletr  10035  xrletr  10036  xgepnf  10044  xlt0neg2  10067  xle0neg2  10069  xaddpnf2  10075  xaddmnf2  10077  xaddid2  10091  elioomnf  10196  ige3m2fz  10277  fzshftral  10336  ige2m1fz1  10337  1fv  10367  4fvwrd4  10368  rebtwn2zlemstep  10505  qbtwnxr  10510  btwnzge0  10553  zmodid2  10607  q2txmodxeq0  10639  frec2uzrand  10660  frecuzrdgtcl  10667  frecfzennn  10681  nn0ennn  10688  uzennn  10691  0exp  10829  sqgt0api  10880  subsq2  10902  qsqeqor  10905  bernneq  10915  faclbnd  10996  faclbnd2  10997  faclbnd3  10998  hashinfuni  11032  hashxp  11083  iswrdiz  11113  lsw0  11154  ccatlid  11176  s1leng  11194  s1fv  11196  s111  11201  pfx0g  11250  2shfti  11385  reim  11406  imcl  11408  crim  11412  caucvgre  11535  rennim  11556  resqrexlemdecn  11566  qabsor  11629  absimle  11638  sqrtthi  11673  sqrtcli  11674  sqrtgt0i  11675  sqrtmsqi  11676  sqrtsqi  11677  sqsqrti  11678  sqrtge0i  11679  absidi  11680  absnidi  11681  xrmaxiflemlub  11802  serclim0  11859  fsum2d  11989  fsumcnv  11991  fsumconst  12008  modfsummodlem1  12010  fsumabs  12019  binom11  12040  prodf1  12096  prodfclim1  12098  prodsnf  12146  fprod2d  12177  fprodcnv  12179  efzval  12237  eftlub  12244  efsep  12245  ef4p  12248  efgt1  12251  reef11  12253  sinf  12258  cosf  12259  efi4p  12271  sinneg  12280  cosneg  12281  efival  12286  efmival  12287  cos01gt0  12317  sin02gt0  12318  absefib  12325  efieq1re  12326  demoivre  12327  demoivreALT  12328  eirraplem  12331  0dvds  12365  odd2np1lem  12426  odd2np1  12427  even2n  12428  mod2eq0even  12432  2teven  12441  opoe  12449  omoe  12450  opeo  12451  omeo  12452  m1exp1  12455  bits0e  12503  bits0o  12504  bitsinv1  12516  gcd0id  12543  gcdid0  12544  1gcd  12556  lcmdvds  12644  isprm2lem  12681  isprm3  12683  prmgt1  12697  coprm  12709  isevengcd2  12723  isoddgcd1  12724  sqpweven  12740  2sqpwodd  12741  pythagtriplem12  12841  pythagtriplem13  12842  pythagtriplem14  12843  pythagtriplem16  12845  pc2dvds  12896  oddprmdvds  12920  pockthi  12924  1arith2  12934  unennn  13011  ctinfomlemom  13041  qnnen  13045  ssnnctlemct  13060  strslfv  13120  strle1g  13182  1strbas  13193  tgval  13338  ismgmn0  13434  mulgval  13702  mulgfng  13704  mulg0  13705  mulg1  13709  mulg2  13711  isnsg  13782  ringidvalg  13967  issrg  13971  subrgpropd  14260  rrgval  14269  islmod  14298  scaffvalg  14313  islssm  14364  sraval  14444  mopnset  14559  metuex  14562  zrhval  14624  zrhvalg  14625  zrhex  14628  psrbag  14676  istopon  14730  eltg4i  14772  eltg3  14774  tg1  14776  tg2  14777  topnex  14803  cldrcl  14819  restsn  14897  lmrcl  14909  metflem  15066  xmetf  15067  ismet2  15071  xmeteq0  15076  xmettri2  15078  xmetpsmet  15086  xmetres2  15096  blfvalps  15102  blex  15104  blvalps  15105  blval  15106  blfps  15126  blf  15127  mopnval  15159  cnbl0  15251  cnblcld  15252  blssioo  15270  resubmet  15273  cncfmet  15309  cnplimcim  15384  cnlimcim  15388  cnlimc  15389  dvfgg  15405  dvfpm  15406  dvfcnpm  15407  dvcj  15426  dvmptfsum  15442  reeff1olem  15488  ef2kpi  15523  sinperlem  15525  sin2kpi  15528  cos2kpi  15529  sinhalfpip  15537  sinhalfpim  15538  coshalfpip  15539  coshalfpim  15540  sincosq1sgn  15543  sinq12gt0  15547  sinkpi  15564  reeflog  15580  relogef  15581  logrpap0b  15593  loggt0b  15608  1cxp  15617  ecxp  15618  2logb9irrap  15694  0sgm  15702  lgsval2lem  15732  m1lgs  15807  1vgrex  15864  upgrfi  15946  umgredgnlp  15996  wlkop  16159  clwwlkn0  16217  djucllem  16346  bdrabexg  16451  bdunexb  16465  peano5set  16485  speano5  16489  bj-omtrans  16501  pw1ninf  16540  pwf1oexmid  16550  nninfsellemeq  16566  iswomninnlem  16603