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  1335  mp3an12  1338  mp3an13  1339  ax9o  1712  sbnfc2  3145  ssdifss  3293  undifss  3531  uneqdifeqim  3536  elssuni  3867  csbexa  4162  difexg  4174  rabexg  4176  abssexg  4215  snexg  4217  copsexg  4277  sotritric  4359  sotritrieq  4360  trsuc  4457  oneli  4463  unexb  4477  opeluu  4485  rabxfr  4505  reuhyp  4507  ordunisuc2r  4550  reg3exmid  4616  brrelex12i  4705  brrelex1i  4706  brrelex2i  4707  xpss2  4774  opabid2  4797  eliunxp  4805  releldmi  4905  relelrni  4906  dmexg  4930  rnexg  4931  elres  4982  resexg  4986  relbrcnvg  5048  brcodir  5057  sotri  5065  sotri2  5067  sotri3  5068  dfrel2  5120  coi1  5185  fco  5423  fssres  5433  fabexg  5445  fvopab3g  5634  mptrcl  5644  mpteqb  5652  elfvmptrab1  5656  ffvelcdmi  5696  fsn2  5736  dfmptg  5741  fvpr1  5766  fvconst2  5778  mptexg  5787  oprabid  5954  ovprc  5957  caovcl  6078  caovass  6084  caovdi  6103  elmpocl  6118  ofexg  6140  resfunexgALT  6165  fo1stresm  6219  fo2ndresm  6220  1stexg  6225  2ndexg  6226  elopabi  6253  mpoexxg  6268  mpoxopn0yelv  6297  rntpos  6315  smores  6350  tfr0dm  6380  tfrlemibxssdm  6385  tfrexlem  6392  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  rdgruledefgg  6433  rdgruledefg  6434  rdgivallem  6439  rdgexg  6447  frec0g  6455  ordgt0ge1  6493  omfnex  6507  oeiv  6514  nna0r  6536  nnm0r  6537  nnsucsssuc  6550  nn2m  6585  nnaordex  6586  nnawordex  6587  ecdmn0m  6636  ecelqsi  6648  ecidg  6658  ectocl  6661  encv  6805  f1oen  6818  ssdomg  6837  map1  6871  fiprc  6874  xpdom1  6894  fict  6929  isinfinf  6958  ac6sfi  6959  xpfi  6993  en1eqsn  7014  fidcenumlemr  7021  fiss  7043  eqinfti  7086  djueq2  7107  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djuf1olem  7119  djulclb  7121  inl11  7131  eldju1st  7137  1stinl  7140  2ndinl  7141  1stinr  7142  2ndinr  7143  ctssdccl  7177  isomnimap  7203  ismkvmap  7220  iswomnimap  7232  djucomen  7283  exmidapne  7327  0nnq  7431  mulidnq  7456  archnqq  7484  prarloclemarch2  7486  nqnq0pi  7505  nq0m0r  7523  nq02m  7532  prarloclemlt  7560  prarloclemn  7566  prarloclem5  7567  addnqprllem  7594  addnqprulem  7595  appdivnq  7630  1idprl  7657  1idpru  7658  addextpr  7688  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemnbj  7734  caucvgprlemloc  7742  caucvgprprlemnbj  7760  caucvgprprlemloc  7770  caucvgprprlemaddq  7775  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemloc  7788  suplocexprlemlub  7791  0nsr  7816  ltsosr  7831  recexgt0sr  7840  prsrpos  7852  caucvgsr  7869  mappsrprg  7871  suplocsrlem  7875  mulresr  7905  axcnre  7948  axpre-ltwlin  7950  mullid  8024  0re  8026  axmulgt0  8098  ltnsym2  8117  eqlei  8120  ltnei  8130  muladd11  8159  cnegex  8204  0cnALT  8216  negcl  8226  negneg  8276  mul02  8413  mulm1  8426  lt0neg2  8496  le0neg2  8498  recexre  8605  recexgt0  8607  mulge0  8646  gt0ap0i  8654  recextlem1  8678  recexap  8680  recclapzi  8764  recap0apzi  8765  recidapzi  8766  divassapzi  8789  divmulapzi  8790  divdirapzi  8791  rerecclapzi  8803  ltp1  8871  recgt0i  8933  ltmul1i  8947  ltdiv1i  8948  ltmuldivi  8949  ltmul2i  8950  lemul1i  8951  lemul2i  8952  sup3exmid  8984  nngt1ne1  9025  nnrecre  9027  nn0ge0  9274  nn0addcl  9284  nn0mulcl  9285  zgt0ge1  9384  dfuzi  9436  eluzel2  9606  eluz2b1  9675  uz2m1nn  9679  elnn0dc  9685  elnndc  9686  nn01to3  9691  zq  9700  nnrecq  9719  rpge0  9741  rpreccl  9755  mnflt  9858  pnfnlt  9862  mnfle  9867  xrlelttr  9881  xrltletr  9882  xrletr  9883  xgepnf  9891  xlt0neg2  9914  xle0neg2  9916  xaddpnf2  9922  xaddmnf2  9924  xaddid2  9938  elioomnf  10043  ige3m2fz  10124  fzshftral  10183  ige2m1fz1  10184  1fv  10214  4fvwrd4  10215  rebtwn2zlemstep  10342  qbtwnxr  10347  btwnzge0  10390  zmodid2  10444  q2txmodxeq0  10476  frec2uzrand  10497  frecuzrdgtcl  10504  frecfzennn  10518  nn0ennn  10525  uzennn  10528  0exp  10666  sqgt0api  10717  subsq2  10739  qsqeqor  10742  bernneq  10752  faclbnd  10833  faclbnd2  10834  faclbnd3  10835  hashinfuni  10869  hashxp  10918  iswrdiz  10942  2shfti  10996  reim  11017  imcl  11019  crim  11023  caucvgre  11146  rennim  11167  resqrexlemdecn  11177  qabsor  11240  absimle  11249  sqrtthi  11284  sqrtcli  11285  sqrtgt0i  11286  sqrtmsqi  11287  sqrtsqi  11288  sqsqrti  11289  sqrtge0i  11290  absidi  11291  absnidi  11292  xrmaxiflemlub  11413  serclim0  11470  fsum2d  11600  fsumcnv  11602  fsumconst  11619  modfsummodlem1  11621  fsumabs  11630  binom11  11651  prodf1  11707  prodfclim1  11709  prodsnf  11757  fprod2d  11788  fprodcnv  11790  efzval  11848  eftlub  11855  efsep  11856  ef4p  11859  efgt1  11862  reef11  11864  sinf  11869  cosf  11870  efi4p  11882  sinneg  11891  cosneg  11892  efival  11897  efmival  11898  cos01gt0  11928  sin02gt0  11929  absefib  11936  efieq1re  11937  demoivre  11938  demoivreALT  11939  eirraplem  11942  0dvds  11976  odd2np1lem  12037  odd2np1  12038  even2n  12039  mod2eq0even  12043  2teven  12052  opoe  12060  omoe  12061  opeo  12062  omeo  12063  m1exp1  12066  bits0e  12113  bits0o  12114  gcd0id  12146  gcdid0  12147  1gcd  12159  lcmdvds  12247  isprm2lem  12284  isprm3  12286  prmgt1  12300  coprm  12312  isevengcd2  12326  isoddgcd1  12327  sqpweven  12343  2sqpwodd  12344  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem16  12448  pc2dvds  12499  oddprmdvds  12523  pockthi  12527  1arith2  12537  unennn  12614  ctinfomlemom  12644  qnnen  12648  ssnnctlemct  12663  strslfv  12723  strle1g  12784  1strbas  12795  tgval  12933  ismgmn0  13001  mulgval  13252  mulgfng  13254  mulg0  13255  mulg1  13259  mulg2  13261  isnsg  13332  ringidvalg  13517  issrg  13521  subrgpropd  13809  rrgval  13818  islmod  13847  scaffvalg  13862  islssm  13913  sraval  13993  mopnset  14108  metuex  14111  zrhval  14173  zrhvalg  14174  zrhex  14177  psrbag  14223  istopon  14249  eltg4i  14291  eltg3  14293  tg1  14295  tg2  14296  topnex  14322  cldrcl  14338  restsn  14416  lmrcl  14427  metflem  14585  xmetf  14586  ismet2  14590  xmeteq0  14595  xmettri2  14597  xmetpsmet  14605  xmetres2  14615  blfvalps  14621  blex  14623  blvalps  14624  blval  14625  blfps  14645  blf  14646  mopnval  14678  cnbl0  14770  cnblcld  14771  blssioo  14789  resubmet  14792  cncfmet  14828  cnplimcim  14903  cnlimcim  14907  cnlimc  14908  dvfgg  14924  dvfpm  14925  dvfcnpm  14926  dvcj  14945  dvmptfsum  14961  reeff1olem  15007  ef2kpi  15042  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  sinhalfpip  15056  sinhalfpim  15057  coshalfpip  15058  coshalfpim  15059  sincosq1sgn  15062  sinq12gt0  15066  sinkpi  15083  reeflog  15099  relogef  15100  logrpap0b  15112  loggt0b  15127  1cxp  15136  ecxp  15137  2logb9irrap  15213  0sgm  15221  lgsval2lem  15251  m1lgs  15326  djucllem  15446  bdrabexg  15552  bdunexb  15566  peano5set  15586  speano5  15590  bj-omtrans  15602  pwf1oexmid  15644  nninfsellemeq  15658  iswomninnlem  15693