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  614  mpjaodan  799  mpd3an3  1349  eueq2dc  2933  csbiegf  3124  difsnb  3761  reusv3i  4490  fimadmfo  5485  fvmpt3  5636  ffvelcdmd  5694  fnressn  5744  fliftel1  5837  f1oiso2  5870  riota5f  5898  1stvalg  6195  2ndvalg  6196  brtpos2  6304  tfrlemibxssdm  6380  dom2lem  6826  php5  6914  nnfi  6928  xpfi  6986  supisoti  7069  ordiso2  7094  omp1eomlem  7153  nnnninfeq2  7188  onenon  7244  oncardval  7246  cardonle  7247  recidnq  7453  archnqq  7477  prarloclemarch2  7479  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  recexprlemex  7697  0idsr  7827  lep1  8864  suprlubex  8971  uz11  9615  xnegid  9925  eluzfz2  10098  fzsuc  10135  fzsuc2  10145  fzp1disj  10146  fzneuz  10167  fzp1nel  10170  exbtwnzlemex  10318  flhalf  10371  modqval  10395  frec2uzsucd  10472  frecuzrdgsuc  10485  uzsinds  10515  seq3p1  10536  seqp1cd  10541  expubnd  10667  iexpcyc  10715  binom2sub1  10725  hashennn  10851  shftfval  10965  shftcan1  10978  cjval  10989  reval  10993  imval  10994  cjmulrcl  11031  addcj  11035  absval  11145  resqrexlemdecn  11156  resqrexlemnmsq  11161  resqrexlemnm  11162  absneg  11194  abscj  11196  sqabsadd  11199  sqabssub  11200  ltabs  11231  dfabsmax  11361  negfi  11371  fsum3  11530  trirecip  11644  fprodseq  11726  efval  11804  ege2le3  11814  efcan  11819  sinval  11845  cosval  11846  efi4p  11860  resin4p  11861  recos4p  11862  sincossq  11891  eirraplem  11920  iddvds  11947  1dvds  11948  bezoutlemstep  12134  coprmgcdb  12226  1idssfct  12253  exprmfct  12276  oddpwdclemdc  12311  phival  12351  odzphi  12384  oddprmdvds  12492  setsn0fun  12655  gsumfzval  12974  0subm  13056  gsumfzz  13067  grprcan  13109  isgrpid2  13112  grpinvid  13132  mulgval  13192  mulgnn0z  13219  0subg  13269  qus0  13305  ghmker  13340  imasabl  13406  mgpplusgg  13420  mgpbasg  13422  mgpscag  13423  mgptsetg  13424  mgpdsg  13426  srgen1zr  13484  opprmulfvalg  13566  opprsllem  13570  1unit  13603  1rinv  13624  subrngmcl  13705  subrg1  13727  subrgmcl  13729  subrgdvds  13731  subrguss  13732  subrginv  13733  subrgdv  13734  subrgunit  13735  subrgugrp  13736  rnrhmsubrg  13748  lmodfopne  13822  lsssn0  13866  lspsn0  13918  lsp0  13919  sralmod  13946  2idlval  13998  cnfldneg  14061  zrhval  14105  cldval  14267  ntrfval  14268  clsfval  14269  neifval  14308  tx1cn  14437  ismet  14512  isxmet  14513  divcnap  14723  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  1lgs  15159  lgs1  15160  bj-charfun  15299  bj-findis  15471