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  3185  ssdifss  3334  undifss  3572  uneqdifeqim  3577  elssuni  3916  csbexa  4213  difexg  4226  rabexg  4228  abssexg  4267  snexg  4269  copsexg  4331  sotritric  4416  sotritrieq  4417  trsuc  4514  oneli  4520  unexb  4534  opeluu  4542  rabxfr  4562  reuhyp  4564  ordunisuc2r  4607  reg3exmid  4673  brrelex12i  4763  brrelex1i  4764  brrelex2i  4765  xpss2  4832  opabid2  4856  eliunxp  4864  releldmi  4966  relelrni  4967  dmexg  4991  rnexg  4992  elres  5044  resexg  5048  relbrcnvg  5110  brcodir  5119  sotri  5127  sotri2  5129  sotri3  5130  dfrel2  5182  coi1  5247  fco  5494  fssres  5506  fabexg  5518  fvopab3g  5712  mptrcl  5722  mpteqb  5730  elfvmptrab1  5734  ffvelcdmi  5774  fsn2  5814  dfmptg  5819  fcof  5825  fvpr1  5850  fvconst2  5862  mptexg  5871  oprabid  6042  ovprc  6046  caovcl  6169  caovass  6175  caovdi  6194  elmpocl  6209  relmptopab  6216  ofexg  6232  resfunexgALT  6262  fo1stresm  6316  fo2ndresm  6317  1stexg  6322  2ndexg  6323  elopabi  6352  mpoexxg  6367  mpoxopn0yelv  6396  rntpos  6414  smores  6449  tfr0dm  6479  tfrlemibxssdm  6484  tfrexlem  6491  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  rdgruledefgg  6532  rdgruledefg  6533  rdgivallem  6538  rdgexg  6546  frec0g  6554  ordgt0ge1  6594  omfnex  6608  oeiv  6615  nna0r  6637  nnm0r  6638  nnsucsssuc  6651  nn2m  6686  nnaordex  6687  nnawordex  6688  ecdmn0m  6737  ecelqsi  6749  ecidg  6759  ectocl  6762  encv  6906  f1oen  6923  ssdomg  6943  map1  6978  fiprc  6981  dom1o  6990  xpdom1  7007  fict  7043  isinfinf  7072  ac6sfi  7073  xpfi  7110  en1eqsn  7131  fidcenumlemr  7138  fiss  7160  eqinfti  7203  djueq2  7224  djulclr  7232  djurclr  7233  djulcl  7234  djurcl  7235  djuf1olem  7236  djulclb  7238  inl11  7248  eldju1st  7254  1stinl  7257  2ndinl  7258  1stinr  7259  2ndinr  7260  ctssdccl  7294  isomnimap  7320  ismkvmap  7337  iswomnimap  7349  finacn  7402  djucomen  7414  exmidapne  7462  0nnq  7567  mulidnq  7592  archnqq  7620  prarloclemarch2  7622  nqnq0pi  7641  nq0m0r  7659  nq02m  7668  prarloclemlt  7696  prarloclemn  7702  prarloclem5  7703  addnqprllem  7730  addnqprulem  7731  appdivnq  7766  1idprl  7793  1idpru  7794  addextpr  7824  cauappcvgprlemdisj  7854  cauappcvgprlemloc  7855  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemnbj  7870  caucvgprlemloc  7878  caucvgprprlemnbj  7896  caucvgprprlemloc  7906  caucvgprprlemaddq  7911  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemloc  7924  suplocexprlemlub  7927  0nsr  7952  ltsosr  7967  recexgt0sr  7976  prsrpos  7988  caucvgsr  8005  mappsrprg  8007  suplocsrlem  8011  mulresr  8041  axcnre  8084  axpre-ltwlin  8086  mullid  8160  0re  8162  axmulgt0  8234  ltnsym2  8253  eqlei  8256  ltnei  8266  muladd11  8295  cnegex  8340  0cnALT  8352  negcl  8362  negneg  8412  mul02  8549  mulm1  8562  lt0neg2  8632  le0neg2  8634  recexre  8741  recexgt0  8743  mulge0  8782  gt0ap0i  8790  recextlem1  8814  recexap  8816  recclapzi  8900  recap0apzi  8901  recidapzi  8902  divassapzi  8925  divmulapzi  8926  divdirapzi  8927  rerecclapzi  8939  ltp1  9007  recgt0i  9069  ltmul1i  9083  ltdiv1i  9084  ltmuldivi  9085  ltmul2i  9086  lemul1i  9087  lemul2i  9088  sup3exmid  9120  nngt1ne1  9161  nnrecre  9163  nn0ge0  9410  nn0addcl  9420  nn0mulcl  9421  zgt0ge1  9521  dfuzi  9573  eluzel2  9743  eluz2b1  9813  uz2m1nn  9817  elnn0dc  9823  elnndc  9824  nn01to3  9829  zq  9838  nnrecq  9857  rpge0  9879  rpreccl  9893  mnflt  9996  pnfnlt  10000  mnfle  10005  xrlelttr  10019  xrltletr  10020  xrletr  10021  xgepnf  10029  xlt0neg2  10052  xle0neg2  10054  xaddpnf2  10060  xaddmnf2  10062  xaddid2  10076  elioomnf  10181  ige3m2fz  10262  fzshftral  10321  ige2m1fz1  10322  1fv  10352  4fvwrd4  10353  rebtwn2zlemstep  10489  qbtwnxr  10494  btwnzge0  10537  zmodid2  10591  q2txmodxeq0  10623  frec2uzrand  10644  frecuzrdgtcl  10651  frecfzennn  10665  nn0ennn  10672  uzennn  10675  0exp  10813  sqgt0api  10864  subsq2  10886  qsqeqor  10889  bernneq  10899  faclbnd  10980  faclbnd2  10981  faclbnd3  10982  hashinfuni  11016  hashxp  11066  iswrdiz  11096  lsw0  11137  ccatlid  11159  s1leng  11177  s1fv  11179  s111  11184  pfx0g  11229  2shfti  11363  reim  11384  imcl  11386  crim  11390  caucvgre  11513  rennim  11534  resqrexlemdecn  11544  qabsor  11607  absimle  11616  sqrtthi  11651  sqrtcli  11652  sqrtgt0i  11653  sqrtmsqi  11654  sqrtsqi  11655  sqsqrti  11656  sqrtge0i  11657  absidi  11658  absnidi  11659  xrmaxiflemlub  11780  serclim0  11837  fsum2d  11967  fsumcnv  11969  fsumconst  11986  modfsummodlem1  11988  fsumabs  11997  binom11  12018  prodf1  12074  prodfclim1  12076  prodsnf  12124  fprod2d  12155  fprodcnv  12157  efzval  12215  eftlub  12222  efsep  12223  ef4p  12226  efgt1  12229  reef11  12231  sinf  12236  cosf  12237  efi4p  12249  sinneg  12258  cosneg  12259  efival  12264  efmival  12265  cos01gt0  12295  sin02gt0  12296  absefib  12303  efieq1re  12304  demoivre  12305  demoivreALT  12306  eirraplem  12309  0dvds  12343  odd2np1lem  12404  odd2np1  12405  even2n  12406  mod2eq0even  12410  2teven  12419  opoe  12427  omoe  12428  opeo  12429  omeo  12430  m1exp1  12433  bits0e  12481  bits0o  12482  bitsinv1  12494  gcd0id  12521  gcdid0  12522  1gcd  12534  lcmdvds  12622  isprm2lem  12659  isprm3  12661  prmgt1  12675  coprm  12687  isevengcd2  12701  isoddgcd1  12702  sqpweven  12718  2sqpwodd  12719  pythagtriplem12  12819  pythagtriplem13  12820  pythagtriplem14  12821  pythagtriplem16  12823  pc2dvds  12874  oddprmdvds  12898  pockthi  12902  1arith2  12912  unennn  12989  ctinfomlemom  13019  qnnen  13023  ssnnctlemct  13038  strslfv  13098  strle1g  13160  1strbas  13171  tgval  13316  ismgmn0  13412  mulgval  13680  mulgfng  13682  mulg0  13683  mulg1  13687  mulg2  13689  isnsg  13760  ringidvalg  13945  issrg  13949  subrgpropd  14238  rrgval  14247  islmod  14276  scaffvalg  14291  islssm  14342  sraval  14422  mopnset  14537  metuex  14540  zrhval  14602  zrhvalg  14603  zrhex  14606  psrbag  14654  istopon  14708  eltg4i  14750  eltg3  14752  tg1  14754  tg2  14755  topnex  14781  cldrcl  14797  restsn  14875  lmrcl  14887  metflem  15044  xmetf  15045  ismet2  15049  xmeteq0  15054  xmettri2  15056  xmetpsmet  15064  xmetres2  15074  blfvalps  15080  blex  15082  blvalps  15083  blval  15084  blfps  15104  blf  15105  mopnval  15137  cnbl0  15229  cnblcld  15230  blssioo  15248  resubmet  15251  cncfmet  15287  cnplimcim  15362  cnlimcim  15366  cnlimc  15367  dvfgg  15383  dvfpm  15384  dvfcnpm  15385  dvcj  15404  dvmptfsum  15420  reeff1olem  15466  ef2kpi  15501  sinperlem  15503  sin2kpi  15506  cos2kpi  15507  sinhalfpip  15515  sinhalfpim  15516  coshalfpip  15517  coshalfpim  15518  sincosq1sgn  15521  sinq12gt0  15525  sinkpi  15542  reeflog  15558  relogef  15559  logrpap0b  15571  loggt0b  15586  1cxp  15595  ecxp  15596  2logb9irrap  15672  0sgm  15680  lgsval2lem  15710  m1lgs  15785  1vgrex  15842  upgrfi  15923  umgredgnlp  15971  wlkop  16120  clwwlkn0  16177  djucllem  16273  bdrabexg  16378  bdunexb  16392  peano5set  16412  speano5  16416  bj-omtrans  16428  pw1ninf  16468  pwf1oexmid  16478  nninfsellemeq  16494  iswomninnlem  16531