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  1337  mp3an12  1340  mp3an13  1341  ax9o  1722  sbnfc2  3162  ssdifss  3311  undifss  3549  uneqdifeqim  3554  elssuni  3892  csbexa  4189  difexg  4201  rabexg  4203  abssexg  4242  snexg  4244  copsexg  4306  sotritric  4389  sotritrieq  4390  trsuc  4487  oneli  4493  unexb  4507  opeluu  4515  rabxfr  4535  reuhyp  4537  ordunisuc2r  4580  reg3exmid  4646  brrelex12i  4735  brrelex1i  4736  brrelex2i  4737  xpss2  4804  opabid2  4827  eliunxp  4835  releldmi  4936  relelrni  4937  dmexg  4961  rnexg  4962  elres  5014  resexg  5018  relbrcnvg  5080  brcodir  5089  sotri  5097  sotri2  5099  sotri3  5100  dfrel2  5152  coi1  5217  fco  5461  fssres  5473  fabexg  5485  fvopab3g  5675  mptrcl  5685  mpteqb  5693  elfvmptrab1  5697  ffvelcdmi  5737  fsn2  5777  dfmptg  5782  fvpr1  5811  fvconst2  5823  mptexg  5832  oprabid  5999  ovprc  6003  caovcl  6124  caovass  6130  caovdi  6149  elmpocl  6164  ofexg  6186  resfunexgALT  6216  fo1stresm  6270  fo2ndresm  6271  1stexg  6276  2ndexg  6277  elopabi  6304  mpoexxg  6319  mpoxopn0yelv  6348  rntpos  6366  smores  6401  tfr0dm  6431  tfrlemibxssdm  6436  tfrexlem  6443  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  rdgruledefgg  6484  rdgruledefg  6485  rdgivallem  6490  rdgexg  6498  frec0g  6506  ordgt0ge1  6544  omfnex  6558  oeiv  6565  nna0r  6587  nnm0r  6588  nnsucsssuc  6601  nn2m  6636  nnaordex  6637  nnawordex  6638  ecdmn0m  6687  ecelqsi  6699  ecidg  6709  ectocl  6712  encv  6856  f1oen  6873  ssdomg  6893  map1  6928  fiprc  6931  xpdom1  6955  fict  6991  isinfinf  7020  ac6sfi  7021  xpfi  7055  en1eqsn  7076  fidcenumlemr  7083  fiss  7105  eqinfti  7148  djueq2  7169  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djuf1olem  7181  djulclb  7183  inl11  7193  eldju1st  7199  1stinl  7202  2ndinl  7203  1stinr  7204  2ndinr  7205  ctssdccl  7239  isomnimap  7265  ismkvmap  7282  iswomnimap  7294  finacn  7347  djucomen  7359  exmidapne  7407  0nnq  7512  mulidnq  7537  archnqq  7565  prarloclemarch2  7567  nqnq0pi  7586  nq0m0r  7604  nq02m  7613  prarloclemlt  7641  prarloclemn  7647  prarloclem5  7648  addnqprllem  7675  addnqprulem  7676  appdivnq  7711  1idprl  7738  1idpru  7739  addextpr  7769  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemnbj  7815  caucvgprlemloc  7823  caucvgprprlemnbj  7841  caucvgprprlemloc  7851  caucvgprprlemaddq  7856  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemloc  7869  suplocexprlemlub  7872  0nsr  7897  ltsosr  7912  recexgt0sr  7921  prsrpos  7933  caucvgsr  7950  mappsrprg  7952  suplocsrlem  7956  mulresr  7986  axcnre  8029  axpre-ltwlin  8031  mullid  8105  0re  8107  axmulgt0  8179  ltnsym2  8198  eqlei  8201  ltnei  8211  muladd11  8240  cnegex  8285  0cnALT  8297  negcl  8307  negneg  8357  mul02  8494  mulm1  8507  lt0neg2  8577  le0neg2  8579  recexre  8686  recexgt0  8688  mulge0  8727  gt0ap0i  8735  recextlem1  8759  recexap  8761  recclapzi  8845  recap0apzi  8846  recidapzi  8847  divassapzi  8870  divmulapzi  8871  divdirapzi  8872  rerecclapzi  8884  ltp1  8952  recgt0i  9014  ltmul1i  9028  ltdiv1i  9029  ltmuldivi  9030  ltmul2i  9031  lemul1i  9032  lemul2i  9033  sup3exmid  9065  nngt1ne1  9106  nnrecre  9108  nn0ge0  9355  nn0addcl  9365  nn0mulcl  9366  zgt0ge1  9466  dfuzi  9518  eluzel2  9688  eluz2b1  9757  uz2m1nn  9761  elnn0dc  9767  elnndc  9768  nn01to3  9773  zq  9782  nnrecq  9801  rpge0  9823  rpreccl  9837  mnflt  9940  pnfnlt  9944  mnfle  9949  xrlelttr  9963  xrltletr  9964  xrletr  9965  xgepnf  9973  xlt0neg2  9996  xle0neg2  9998  xaddpnf2  10004  xaddmnf2  10006  xaddid2  10020  elioomnf  10125  ige3m2fz  10206  fzshftral  10265  ige2m1fz1  10266  1fv  10296  4fvwrd4  10297  rebtwn2zlemstep  10432  qbtwnxr  10437  btwnzge0  10480  zmodid2  10534  q2txmodxeq0  10566  frec2uzrand  10587  frecuzrdgtcl  10594  frecfzennn  10608  nn0ennn  10615  uzennn  10618  0exp  10756  sqgt0api  10807  subsq2  10829  qsqeqor  10832  bernneq  10842  faclbnd  10923  faclbnd2  10924  faclbnd3  10925  hashinfuni  10959  hashxp  11008  iswrdiz  11038  lsw0  11078  ccatlid  11100  s1leng  11116  s1fv  11118  s111  11123  pfx0g  11167  2shfti  11257  reim  11278  imcl  11280  crim  11284  caucvgre  11407  rennim  11428  resqrexlemdecn  11438  qabsor  11501  absimle  11510  sqrtthi  11545  sqrtcli  11546  sqrtgt0i  11547  sqrtmsqi  11548  sqrtsqi  11549  sqsqrti  11550  sqrtge0i  11551  absidi  11552  absnidi  11553  xrmaxiflemlub  11674  serclim0  11731  fsum2d  11861  fsumcnv  11863  fsumconst  11880  modfsummodlem1  11882  fsumabs  11891  binom11  11912  prodf1  11968  prodfclim1  11970  prodsnf  12018  fprod2d  12049  fprodcnv  12051  efzval  12109  eftlub  12116  efsep  12117  ef4p  12120  efgt1  12123  reef11  12125  sinf  12130  cosf  12131  efi4p  12143  sinneg  12152  cosneg  12153  efival  12158  efmival  12159  cos01gt0  12189  sin02gt0  12190  absefib  12197  efieq1re  12198  demoivre  12199  demoivreALT  12200  eirraplem  12203  0dvds  12237  odd2np1lem  12298  odd2np1  12299  even2n  12300  mod2eq0even  12304  2teven  12313  opoe  12321  omoe  12322  opeo  12323  omeo  12324  m1exp1  12327  bits0e  12375  bits0o  12376  bitsinv1  12388  gcd0id  12415  gcdid0  12416  1gcd  12428  lcmdvds  12516  isprm2lem  12553  isprm3  12555  prmgt1  12569  coprm  12581  isevengcd2  12595  isoddgcd1  12596  sqpweven  12612  2sqpwodd  12613  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem16  12717  pc2dvds  12768  oddprmdvds  12792  pockthi  12796  1arith2  12806  unennn  12883  ctinfomlemom  12913  qnnen  12917  ssnnctlemct  12932  strslfv  12992  strle1g  13053  1strbas  13064  tgval  13209  ismgmn0  13305  mulgval  13573  mulgfng  13575  mulg0  13576  mulg1  13580  mulg2  13582  isnsg  13653  ringidvalg  13838  issrg  13842  subrgpropd  14130  rrgval  14139  islmod  14168  scaffvalg  14183  islssm  14234  sraval  14314  mopnset  14429  metuex  14432  zrhval  14494  zrhvalg  14495  zrhex  14498  psrbag  14546  istopon  14600  eltg4i  14642  eltg3  14644  tg1  14646  tg2  14647  topnex  14673  cldrcl  14689  restsn  14767  lmrcl  14778  metflem  14936  xmetf  14937  ismet2  14941  xmeteq0  14946  xmettri2  14948  xmetpsmet  14956  xmetres2  14966  blfvalps  14972  blex  14974  blvalps  14975  blval  14976  blfps  14996  blf  14997  mopnval  15029  cnbl0  15121  cnblcld  15122  blssioo  15140  resubmet  15143  cncfmet  15179  cnplimcim  15254  cnlimcim  15258  cnlimc  15259  dvfgg  15275  dvfpm  15276  dvfcnpm  15277  dvcj  15296  dvmptfsum  15312  reeff1olem  15358  ef2kpi  15393  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  sinhalfpip  15407  sinhalfpim  15408  coshalfpip  15409  coshalfpim  15410  sincosq1sgn  15413  sinq12gt0  15417  sinkpi  15434  reeflog  15450  relogef  15451  logrpap0b  15463  loggt0b  15478  1cxp  15487  ecxp  15488  2logb9irrap  15564  0sgm  15572  lgsval2lem  15602  m1lgs  15677  1vgrex  15734  upgrfi  15813  umgredgnlp  15856  djucllem  15936  bdrabexg  16041  bdunexb  16055  peano5set  16075  speano5  16079  bj-omtrans  16091  dom1o  16128  pwf1oexmid  16138  nninfsellemeq  16153  iswomninnlem  16190