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  1361  mp3an12  1364  mp3an13  1365  ax9o  1746  sbnfc2  3201  ssdifss  3351  undifss  3592  uneqdifeqim  3597  elssuni  3944  csbexa  4241  difexg  4254  rabexg  4257  abssexg  4297  snexg  4299  copsexg  4362  sotritric  4447  sotritrieq  4448  trsuc  4545  oneli  4551  unexb  4565  opeluu  4573  rabxfr  4593  reuhyp  4595  ordunisuc2r  4638  reg3exmid  4704  brrelex12i  4794  brrelex1i  4795  brrelex2i  4796  xpss2  4863  opabid2  4888  eliunxp  4896  releldmi  4998  relelrni  4999  dmexg  5023  rnexg  5024  elres  5076  resexg  5080  relbrcnvg  5143  brcodir  5152  sotri  5160  sotri2  5162  sotri3  5163  dfrel2  5215  coi1  5280  fco  5529  fssres  5542  fabexg  5556  fvopab3g  5752  mptrcl  5762  mpteqb  5770  elfvmptrab1  5774  ffvelcdmi  5813  fsn2  5853  dfmptg  5859  fcof  5865  fvpr1  5890  fvconst2  5902  mptexg  5913  oprabid  6084  ovprc  6088  caovcl  6211  caovass  6217  caovdi  6236  elmpocl  6251  relmptopab  6258  ofexg  6273  resfunexgALT  6303  fo1stresm  6357  fo2ndresm  6358  1stexg  6363  2ndexg  6364  elopabi  6393  mpoexxg  6408  elmpom  6436  supp0  6440  mpoxopn0yelv  6472  rntpos  6490  smores  6525  tfr0dm  6555  tfrlemibxssdm  6560  tfrexlem  6567  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  rdgruledefgg  6608  rdgruledefg  6609  rdgivallem  6614  rdgexg  6622  frec0g  6630  ordgt0ge1  6670  omfnex  6684  oeiv  6691  nna0r  6713  nnm0r  6714  nnsucsssuc  6727  nn2m  6762  nnaordex  6763  nnawordex  6764  ecdmn0m  6813  ecelqsi  6825  ecidg  6835  ectocl  6838  encv  6983  f1oen  7000  ssdomg  7020  map1  7056  fiprc  7059  dom1o  7071  xpdom1  7088  fict  7125  isinfinf  7156  ac6sfi  7157  xpfi  7194  en1eqsn  7220  fidcenumlemr  7227  fiss  7266  fipwfi  7274  eqinfti  7313  djueq2  7334  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djuf1olem  7346  djulclb  7348  inl11  7358  eldju1st  7364  1stinl  7367  2ndinl  7368  1stinr  7369  2ndinr  7370  ctssdccl  7404  isomnimap  7430  ismkvmap  7447  iswomnimap  7459  finacn  7513  djucomen  7525  exmidapne  7579  0nnq  7684  mulidnq  7709  archnqq  7737  prarloclemarch2  7739  nqnq0pi  7758  nq0m0r  7776  nq02m  7785  prarloclemlt  7813  prarloclemn  7819  prarloclem5  7820  addnqprllem  7847  addnqprulem  7848  appdivnq  7883  1idprl  7910  1idpru  7911  addextpr  7941  cauappcvgprlemdisj  7971  cauappcvgprlemloc  7972  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  caucvgprlemnbj  7987  caucvgprlemloc  7995  caucvgprprlemnbj  8013  caucvgprprlemloc  8023  caucvgprprlemaddq  8028  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemloc  8041  suplocexprlemlub  8044  0nsr  8069  ltsosr  8084  recexgt0sr  8093  prsrpos  8105  caucvgsr  8122  mappsrprg  8124  suplocsrlem  8128  mulresr  8158  axcnre  8201  axpre-ltwlin  8203  mullid  8277  0re  8279  axmulgt0  8350  ltnsym2  8369  eqlei  8372  ltnei  8382  muladd11  8411  cnegex  8456  0cnALT  8468  negcl  8478  negneg  8528  mul02  8665  mulm1  8678  lt0neg2  8748  le0neg2  8750  recexre  8857  recexgt0  8859  mulge0  8898  gt0ap0i  8906  recextlem1  8930  recexap  8932  recclapzi  9016  recap0apzi  9017  recidapzi  9018  divassapzi  9041  divmulapzi  9042  divdirapzi  9043  rerecclapzi  9055  ltp1  9123  recgt0i  9185  ltmul1i  9199  ltdiv1i  9200  ltmuldivi  9201  ltmul2i  9202  lemul1i  9203  lemul2i  9204  sup3exmid  9236  nngt1ne1  9277  nnrecre  9279  nn0ge0  9526  nn0addcl  9536  nn0mulcl  9537  zgt0ge1  9641  dfuzi  9694  eluzel2  9864  eluz2b1  9939  uz2m1nn  9943  elnn0dc  9949  elnndc  9950  nn01to3  9955  zq  9964  nnrecq  9983  rpge0  10005  rpreccl  10019  mnflt  10122  pnfnlt  10126  mnfle  10131  xrlelttr  10145  xrltletr  10146  xrletr  10147  xgepnf  10155  xlt0neg2  10178  xle0neg2  10180  xaddpnf2  10186  xaddmnf2  10188  xaddid2  10202  elioomnf  10307  ige3m2fz  10389  fzshftral  10449  ige2m1fz1  10450  1fv  10480  4fvwrd4  10481  rebtwn2zlemstep  10619  qbtwnxr  10624  btwnzge0  10667  zmodid2  10721  q2txmodxeq0  10753  frec2uzrand  10774  frecuzrdgtcl  10781  frecfzennn  10795  nn0ennn  10802  uzennn  10805  0exp  10943  sqgt0api  10994  subsq2  11016  qsqeqor  11019  bernneq  11030  faclbnd  11111  faclbnd2  11112  faclbnd3  11113  hashinfuni  11148  hashxp  11199  hashpwfi  11201  iswrdiz  11239  lsw0  11280  ccatlid  11302  s1leng  11320  s1fv  11322  s111  11327  pfx0g  11376  2shfti  11524  reim  11545  imcl  11547  crim  11551  caucvgre  11674  rennim  11695  resqrexlemdecn  11705  qabsor  11768  absimle  11777  sqrtthi  11812  sqrtcli  11813  sqrtgt0i  11814  sqrtmsqi  11815  sqrtsqi  11816  sqsqrti  11817  sqrtge0i  11818  absidi  11819  absnidi  11820  xrmaxiflemlub  11941  serclim0  11998  fsum2d  12129  fsumcnv  12131  fsumconst  12148  modfsummodlem1  12150  fsumabs  12159  binom11  12180  prodf1  12236  prodfclim1  12238  prodsnf  12286  fprod2d  12317  fprodcnv  12319  efzval  12377  eftlub  12384  efsep  12385  ef4p  12388  efgt1  12391  reef11  12393  sinf  12398  cosf  12399  efi4p  12411  sinneg  12420  cosneg  12421  efival  12426  efmival  12427  cos01gt0  12457  sin02gt0  12458  absefib  12465  efieq1re  12466  demoivre  12467  demoivreALT  12468  eirraplem  12471  0dvds  12505  odd2np1lem  12566  odd2np1  12567  even2n  12568  mod2eq0even  12572  2teven  12581  opoe  12589  omoe  12590  opeo  12591  omeo  12592  m1exp1  12595  bits0e  12643  bits0o  12644  bitsinv1  12656  gcd0id  12683  gcdid0  12684  1gcd  12696  lcmdvds  12784  isprm2lem  12821  isprm3  12823  prmgt1  12837  coprm  12849  isevengcd2  12863  isoddgcd1  12864  sqpweven  12880  2sqpwodd  12881  pythagtriplem12  12981  pythagtriplem13  12982  pythagtriplem14  12983  pythagtriplem16  12985  pc2dvds  13036  oddprmdvds  13060  pockthi  13064  1arith2  13074  unennn  13169  ctinfomlemom  13199  qnnen  13203  ssnnctlemct  13218  strslfv  13278  strle1g  13340  1strbas  13351  tgval  13496  ismgmn0  13592  mulgval  13860  mulgfng  13862  mulg0  13863  mulg1  13867  mulg2  13869  isnsg  13940  ringidvalg  14126  issrg  14130  subrgpropd  14421  rrgval  14430  islmod  14488  scaffvalg  14503  islssm  14554  sraval  14634  mopnset  14749  metuex  14752  zrhval  14814  zrhvalg  14815  zrhex  14818  psrbag  14866  psrbagaddclfi  14874  istopon  14927  eltg4i  14969  eltg3  14971  tg1  14973  tg2  14974  topnex  15000  cldrcl  15016  restsn  15094  lmrcl  15106  metflem  15263  xmetf  15264  ismet2  15268  xmeteq0  15273  xmettri2  15275  xmetpsmet  15283  xmetres2  15293  blfvalps  15299  blex  15301  blvalps  15302  blval  15303  blfps  15323  blf  15324  mopnval  15356  cnbl0  15448  cnblcld  15449  blssioo  15467  resubmet  15470  cncfmet  15506  cnplimcim  15581  cnlimcim  15585  cnlimc  15586  dvfgg  15602  dvfpm  15603  dvfcnpm  15604  dvcj  15623  dvmptfsum  15639  reeff1olem  15685  ef2kpi  15720  sinperlem  15722  sin2kpi  15725  cos2kpi  15726  sinhalfpip  15734  sinhalfpim  15735  coshalfpip  15736  coshalfpim  15737  sincosq1sgn  15740  sinq12gt0  15744  sinkpi  15761  reeflog  15777  relogef  15778  logrpap0b  15790  loggt0b  15805  1cxp  15814  ecxp  15815  2logb9irrap  15891  0sgm  15902  lgsval2lem  15932  m1lgs  16007  1vgrex  16064  upgrfi  16146  umgredgnlp  16196  wlkop  16392  clwwlkn0  16452  djucllem  16621  bdrabexg  16725  bdunexb  16739  peano5set  16759  speano5  16763  bj-omtrans  16775  pw1ninf  16814  pwf1oexmid  16822  nninfsellemeq  16841  iswomninnlem  16883