Theorem mpdan 421

Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
mpdan.1	⊢ (𝜑 → 𝜓)
mpdan.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mpdan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜑 → 𝜑)
2		mpdan.1	. 2 ⊢ (𝜑 → 𝜓)
3		mpdan.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 411	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:  mpidan  423  mpan2  425  biadanid  616  mpjaodan  803  mpd3an3  1372  eueq2dc  2977  csbiegf  3169  difsnb  3814  reusv3i  4554  fimadmfo  5565  fvmpt3  5721  ffvelcdmd  5779  fnressn  5835  fliftel1  5930  f1oiso2  5963  riota5f  5993  1stvalg  6300  2ndvalg  6301  brtpos2  6412  tfrlemibxssdm  6488  dom2lem  6940  php5  7039  nnfi  7054  xpfi  7119  supisoti  7203  ordiso2  7228  omp1eomlem  7287  nnnninfeq2  7322  onenon  7382  oncardval  7384  cardonle  7385  recidnq  7606  archnqq  7630  prarloclemarch2  7632  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  recexprlemex  7850  0idsr  7980  lep1  9018  suprlubex  9125  uz11  9772  xnegid  10087  eluzfz2  10260  fzsuc  10297  fzsuc2  10307  fzp1disj  10308  fzneuz  10329  fzp1nel  10332  exbtwnzlemex  10502  flhalf  10555  modqval  10579  frec2uzsucd  10656  frecuzrdgsuc  10669  uzsinds  10699  seq3p1  10720  seqp1cd  10725  expubnd  10851  iexpcyc  10899  binom2sub1  10909  hashennn  11035  lswwrd  11153  eqs1  11198  pfxid  11260  wrdind  11296  wrd2ind  11297  pfxccatpfx2  11311  swrdccat3blem  11313  shftfval  11375  shftcan1  11388  cjval  11399  reval  11403  imval  11404  cjmulrcl  11441  addcj  11445  absval  11555  resqrexlemdecn  11566  resqrexlemnmsq  11571  resqrexlemnm  11572  absneg  11604  abscj  11606  sqabsadd  11609  sqabssub  11610  ltabs  11641  dfabsmax  11771  negfi  11782  fsum3  11941  trirecip  12055  fprodseq  12137  efval  12215  ege2le3  12225  efcan  12230  sinval  12256  cosval  12257  efi4p  12271  resin4p  12272  recos4p  12273  sincossq  12302  eirraplem  12331  iddvds  12358  1dvds  12359  bezoutlemstep  12561  coprmgcdb  12653  1idssfct  12680  exprmfct  12703  oddpwdclemdc  12738  phival  12778  odzphi  12812  oddprmdvds  12920  setsn0fun  13112  gsumfzval  13467  0subm  13560  gsumfzz  13571  grprcan  13613  isgrpid2  13616  grpinvid  13636  mulgval  13702  mulgnn0z  13729  0subg  13779  qus0  13815  ghmker  13850  imasabl  13916  mgpplusgg  13930  mgpbasg  13932  mgpscag  13933  mgptsetg  13934  mgpdsg  13936  srgen1zr  13994  opprmulfvalg  14076  opprsllem  14080  1unit  14114  1rinv  14135  subrngmcl  14216  subrg1  14238  subrgmcl  14240  subrgdvds  14242  subrguss  14243  subrginv  14244  subrgdv  14245  subrgunit  14246  subrgugrp  14247  rnrhmsubrg  14259  lmodfopne  14333  lsssn0  14377  lspsn0  14429  lsp0  14430  sralmod  14457  2idlval  14509  cnfldneg  14580  zrhval  14624  cldval  14816  ntrfval  14817  clsfval  14818  neifval  14857  tx1cn  14986  ismet  15061  isxmet  15062  divcnap  15282  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  sgmnncl  15705  1lgs  15765  lgs1  15766  uhgredgiedgb  15978  uhgriedg0edg0  15979  wlklenvm1  16152  wlklenvm1g  16153  wlkl1loop  16169  wlklenvclwlk  16184  umgrclwwlkge2  16211  clwwlknp  16226  bj-charfun  16352  bj-findis  16524