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  800  mpd3an3  1351  eueq2dc  2947  csbiegf  3138  difsnb  3778  reusv3i  4510  fimadmfo  5514  fvmpt3  5665  ffvelcdmd  5723  fnressn  5777  fliftel1  5870  f1oiso2  5903  riota5f  5931  1stvalg  6235  2ndvalg  6236  brtpos2  6344  tfrlemibxssdm  6420  dom2lem  6870  php5  6962  nnfi  6976  xpfi  7036  supisoti  7119  ordiso2  7144  omp1eomlem  7203  nnnninfeq2  7238  onenon  7298  oncardval  7300  cardonle  7301  recidnq  7513  archnqq  7537  prarloclemarch2  7539  recexprlem1ssl  7753  recexprlem1ssu  7754  recexprlemss1l  7755  recexprlemss1u  7756  recexprlemex  7757  0idsr  7887  lep1  8925  suprlubex  9032  uz11  9678  xnegid  9988  eluzfz2  10161  fzsuc  10198  fzsuc2  10208  fzp1disj  10209  fzneuz  10230  fzp1nel  10233  exbtwnzlemex  10399  flhalf  10452  modqval  10476  frec2uzsucd  10553  frecuzrdgsuc  10566  uzsinds  10596  seq3p1  10617  seqp1cd  10622  expubnd  10748  iexpcyc  10796  binom2sub1  10806  hashennn  10932  lswwrd  11047  eqs1  11090  pfxid  11145  shftfval  11176  shftcan1  11189  cjval  11200  reval  11204  imval  11205  cjmulrcl  11242  addcj  11246  absval  11356  resqrexlemdecn  11367  resqrexlemnmsq  11372  resqrexlemnm  11373  absneg  11405  abscj  11407  sqabsadd  11410  sqabssub  11411  ltabs  11442  dfabsmax  11572  negfi  11583  fsum3  11742  trirecip  11856  fprodseq  11938  efval  12016  ege2le3  12026  efcan  12031  sinval  12057  cosval  12058  efi4p  12072  resin4p  12073  recos4p  12074  sincossq  12103  eirraplem  12132  iddvds  12159  1dvds  12160  bezoutlemstep  12362  coprmgcdb  12454  1idssfct  12481  exprmfct  12504  oddpwdclemdc  12539  phival  12579  odzphi  12613  oddprmdvds  12721  setsn0fun  12913  gsumfzval  13267  0subm  13360  gsumfzz  13371  grprcan  13413  isgrpid2  13416  grpinvid  13436  mulgval  13502  mulgnn0z  13529  0subg  13579  qus0  13615  ghmker  13650  imasabl  13716  mgpplusgg  13730  mgpbasg  13732  mgpscag  13733  mgptsetg  13734  mgpdsg  13736  srgen1zr  13794  opprmulfvalg  13876  opprsllem  13880  1unit  13913  1rinv  13934  subrngmcl  14015  subrg1  14037  subrgmcl  14039  subrgdvds  14041  subrguss  14042  subrginv  14043  subrgdv  14044  subrgunit  14045  subrgugrp  14046  rnrhmsubrg  14058  lmodfopne  14132  lsssn0  14176  lspsn0  14228  lsp0  14229  sralmod  14256  2idlval  14308  cnfldneg  14379  zrhval  14423  cldval  14615  ntrfval  14616  clsfval  14617  neifval  14656  tx1cn  14785  ismet  14860  isxmet  14861  divcnap  15081  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  sgmnncl  15504  1lgs  15564  lgs1  15565  bj-charfun  15817  bj-findis  15989