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  3294  undifss  3532  uneqdifeqim  3537  elssuni  3868  csbexa  4163  difexg  4175  rabexg  4177  abssexg  4216  snexg  4218  copsexg  4278  sotritric  4360  sotritrieq  4361  trsuc  4458  oneli  4464  unexb  4478  opeluu  4486  rabxfr  4506  reuhyp  4508  ordunisuc2r  4551  reg3exmid  4617  brrelex12i  4706  brrelex1i  4707  brrelex2i  4708  xpss2  4775  opabid2  4798  eliunxp  4806  releldmi  4906  relelrni  4907  dmexg  4931  rnexg  4932  elres  4983  resexg  4987  relbrcnvg  5049  brcodir  5058  sotri  5066  sotri2  5068  sotri3  5069  dfrel2  5121  coi1  5186  fco  5426  fssres  5436  fabexg  5448  fvopab3g  5637  mptrcl  5647  mpteqb  5655  elfvmptrab1  5659  ffvelcdmi  5699  fsn2  5739  dfmptg  5744  fvpr1  5769  fvconst2  5781  mptexg  5790  oprabid  5957  ovprc  5961  caovcl  6082  caovass  6088  caovdi  6107  elmpocl  6122  ofexg  6144  resfunexgALT  6174  fo1stresm  6228  fo2ndresm  6229  1stexg  6234  2ndexg  6235  elopabi  6262  mpoexxg  6277  mpoxopn0yelv  6306  rntpos  6324  smores  6359  tfr0dm  6389  tfrlemibxssdm  6394  tfrexlem  6401  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  rdgruledefgg  6442  rdgruledefg  6443  rdgivallem  6448  rdgexg  6456  frec0g  6464  ordgt0ge1  6502  omfnex  6516  oeiv  6523  nna0r  6545  nnm0r  6546  nnsucsssuc  6559  nn2m  6594  nnaordex  6595  nnawordex  6596  ecdmn0m  6645  ecelqsi  6657  ecidg  6667  ectocl  6670  encv  6814  f1oen  6827  ssdomg  6846  map1  6880  fiprc  6883  xpdom1  6903  fict  6938  isinfinf  6967  ac6sfi  6968  xpfi  7002  en1eqsn  7023  fidcenumlemr  7030  fiss  7052  eqinfti  7095  djueq2  7116  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuf1olem  7128  djulclb  7130  inl11  7140  eldju1st  7146  1stinl  7149  2ndinl  7150  1stinr  7151  2ndinr  7152  ctssdccl  7186  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  finacn  7287  djucomen  7299  exmidapne  7343  0nnq  7448  mulidnq  7473  archnqq  7501  prarloclemarch2  7503  nqnq0pi  7522  nq0m0r  7540  nq02m  7549  prarloclemlt  7577  prarloclemn  7583  prarloclem5  7584  addnqprllem  7611  addnqprulem  7612  appdivnq  7647  1idprl  7674  1idpru  7675  addextpr  7705  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemnbj  7751  caucvgprlemloc  7759  caucvgprprlemnbj  7777  caucvgprprlemloc  7787  caucvgprprlemaddq  7792  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemloc  7805  suplocexprlemlub  7808  0nsr  7833  ltsosr  7848  recexgt0sr  7857  prsrpos  7869  caucvgsr  7886  mappsrprg  7888  suplocsrlem  7892  mulresr  7922  axcnre  7965  axpre-ltwlin  7967  mullid  8041  0re  8043  axmulgt0  8115  ltnsym2  8134  eqlei  8137  ltnei  8147  muladd11  8176  cnegex  8221  0cnALT  8233  negcl  8243  negneg  8293  mul02  8430  mulm1  8443  lt0neg2  8513  le0neg2  8515  recexre  8622  recexgt0  8624  mulge0  8663  gt0ap0i  8671  recextlem1  8695  recexap  8697  recclapzi  8781  recap0apzi  8782  recidapzi  8783  divassapzi  8806  divmulapzi  8807  divdirapzi  8808  rerecclapzi  8820  ltp1  8888  recgt0i  8950  ltmul1i  8964  ltdiv1i  8965  ltmuldivi  8966  ltmul2i  8967  lemul1i  8968  lemul2i  8969  sup3exmid  9001  nngt1ne1  9042  nnrecre  9044  nn0ge0  9291  nn0addcl  9301  nn0mulcl  9302  zgt0ge1  9401  dfuzi  9453  eluzel2  9623  eluz2b1  9692  uz2m1nn  9696  elnn0dc  9702  elnndc  9703  nn01to3  9708  zq  9717  nnrecq  9736  rpge0  9758  rpreccl  9772  mnflt  9875  pnfnlt  9879  mnfle  9884  xrlelttr  9898  xrltletr  9899  xrletr  9900  xgepnf  9908  xlt0neg2  9931  xle0neg2  9933  xaddpnf2  9939  xaddmnf2  9941  xaddid2  9955  elioomnf  10060  ige3m2fz  10141  fzshftral  10200  ige2m1fz1  10201  1fv  10231  4fvwrd4  10232  rebtwn2zlemstep  10359  qbtwnxr  10364  btwnzge0  10407  zmodid2  10461  q2txmodxeq0  10493  frec2uzrand  10514  frecuzrdgtcl  10521  frecfzennn  10535  nn0ennn  10542  uzennn  10545  0exp  10683  sqgt0api  10734  subsq2  10756  qsqeqor  10759  bernneq  10769  faclbnd  10850  faclbnd2  10851  faclbnd3  10852  hashinfuni  10886  hashxp  10935  iswrdiz  10959  2shfti  11013  reim  11034  imcl  11036  crim  11040  caucvgre  11163  rennim  11184  resqrexlemdecn  11194  qabsor  11257  absimle  11266  sqrtthi  11301  sqrtcli  11302  sqrtgt0i  11303  sqrtmsqi  11304  sqrtsqi  11305  sqsqrti  11306  sqrtge0i  11307  absidi  11308  absnidi  11309  xrmaxiflemlub  11430  serclim0  11487  fsum2d  11617  fsumcnv  11619  fsumconst  11636  modfsummodlem1  11638  fsumabs  11647  binom11  11668  prodf1  11724  prodfclim1  11726  prodsnf  11774  fprod2d  11805  fprodcnv  11807  efzval  11865  eftlub  11872  efsep  11873  ef4p  11876  efgt1  11879  reef11  11881  sinf  11886  cosf  11887  efi4p  11899  sinneg  11908  cosneg  11909  efival  11914  efmival  11915  cos01gt0  11945  sin02gt0  11946  absefib  11953  efieq1re  11954  demoivre  11955  demoivreALT  11956  eirraplem  11959  0dvds  11993  odd2np1lem  12054  odd2np1  12055  even2n  12056  mod2eq0even  12060  2teven  12069  opoe  12077  omoe  12078  opeo  12079  omeo  12080  m1exp1  12083  bits0e  12131  bits0o  12132  bitsinv1  12144  gcd0id  12171  gcdid0  12172  1gcd  12184  lcmdvds  12272  isprm2lem  12309  isprm3  12311  prmgt1  12325  coprm  12337  isevengcd2  12351  isoddgcd1  12352  sqpweven  12368  2sqpwodd  12369  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem16  12473  pc2dvds  12524  oddprmdvds  12548  pockthi  12552  1arith2  12562  unennn  12639  ctinfomlemom  12669  qnnen  12673  ssnnctlemct  12688  strslfv  12748  strle1g  12809  1strbas  12820  tgval  12964  ismgmn0  13060  mulgval  13328  mulgfng  13330  mulg0  13331  mulg1  13335  mulg2  13337  isnsg  13408  ringidvalg  13593  issrg  13597  subrgpropd  13885  rrgval  13894  islmod  13923  scaffvalg  13938  islssm  13989  sraval  14069  mopnset  14184  metuex  14187  zrhval  14249  zrhvalg  14250  zrhex  14253  psrbag  14299  istopon  14333  eltg4i  14375  eltg3  14377  tg1  14379  tg2  14380  topnex  14406  cldrcl  14422  restsn  14500  lmrcl  14511  metflem  14669  xmetf  14670  ismet2  14674  xmeteq0  14679  xmettri2  14681  xmetpsmet  14689  xmetres2  14699  blfvalps  14705  blex  14707  blvalps  14708  blval  14709  blfps  14729  blf  14730  mopnval  14762  cnbl0  14854  cnblcld  14855  blssioo  14873  resubmet  14876  cncfmet  14912  cnplimcim  14987  cnlimcim  14991  cnlimc  14992  dvfgg  15008  dvfpm  15009  dvfcnpm  15010  dvcj  15029  dvmptfsum  15045  reeff1olem  15091  ef2kpi  15126  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  sinhalfpip  15140  sinhalfpim  15141  coshalfpip  15142  coshalfpim  15143  sincosq1sgn  15146  sinq12gt0  15150  sinkpi  15167  reeflog  15183  relogef  15184  logrpap0b  15196  loggt0b  15211  1cxp  15220  ecxp  15221  2logb9irrap  15297  0sgm  15305  lgsval2lem  15335  m1lgs  15410  djucllem  15530  bdrabexg  15636  bdunexb  15650  peano5set  15670  speano5  15674  bj-omtrans  15686  pwf1oexmid  15730  nninfsellemeq  15745  iswomninnlem  15780