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  1348  eueq2dc  2922  csbiegf  3112  difsnb  3747  reusv3i  4471  fvmpt3  5608  ffvelcdmd  5665  fnressn  5715  fliftel1  5808  f1oiso2  5841  riota5f  5868  1stvalg  6157  2ndvalg  6158  brtpos2  6266  tfrlemibxssdm  6342  dom2lem  6786  php5  6872  nnfi  6886  xpfi  6943  supisoti  7023  ordiso2  7048  omp1eomlem  7107  nnnninfeq2  7141  onenon  7197  oncardval  7199  cardonle  7200  recidnq  7406  archnqq  7430  prarloclemarch2  7432  recexprlem1ssl  7646  recexprlem1ssu  7647  recexprlemss1l  7648  recexprlemss1u  7649  recexprlemex  7650  0idsr  7780  lep1  8816  suprlubex  8923  uz11  9564  xnegid  9873  eluzfz2  10046  fzsuc  10083  fzsuc2  10093  fzp1disj  10094  fzneuz  10115  fzp1nel  10118  exbtwnzlemex  10264  flhalf  10316  modqval  10338  frec2uzsucd  10415  frecuzrdgsuc  10428  uzsinds  10456  seq3p1  10476  seqp1cd  10480  expubnd  10591  iexpcyc  10639  binom2sub1  10649  hashennn  10774  shftfval  10844  shftcan1  10857  cjval  10868  reval  10872  imval  10873  cjmulrcl  10910  addcj  10914  absval  11024  resqrexlemdecn  11035  resqrexlemnmsq  11040  resqrexlemnm  11041  absneg  11073  abscj  11075  sqabsadd  11078  sqabssub  11079  ltabs  11110  dfabsmax  11240  negfi  11250  fsum3  11409  trirecip  11523  fprodseq  11605  efval  11683  ege2le3  11693  efcan  11698  sinval  11724  cosval  11725  efi4p  11739  resin4p  11740  recos4p  11741  sincossq  11770  eirraplem  11798  iddvds  11825  1dvds  11826  bezoutlemstep  12012  coprmgcdb  12102  1idssfct  12129  exprmfct  12152  oddpwdclemdc  12187  phival  12227  odzphi  12260  oddprmdvds  12366  setsn0fun  12513  0subm  12893  grprcan  12934  isgrpid2  12937  grpinvid  12957  mulgval  13017  mulgnn0z  13042  0subg  13091  imasabl  13171  mgpplusgg  13176  mgpbasg  13178  mgpscag  13179  mgptsetg  13180  mgpdsg  13182  srgen1zr  13240  opprmulfvalg  13318  opprsllem  13322  1unit  13355  1rinv  13376  subrngmcl  13429  subrg1  13451  subrgmcl  13453  subrgdvds  13455  subrguss  13456  subrginv  13457  subrgdv  13458  subrgunit  13459  subrgugrp  13460  lmodfopne  13515  lsssn0  13559  lspsn0  13611  lsp0  13612  sralmod  13639  cnfldneg  13749  cldval  13895  ntrfval  13896  clsfval  13897  neifval  13936  tx1cn  14065  ismet  14140  isxmet  14141  divcnap  14351  dvaddxxbr  14461  dvmulxxbr  14462  dvcoapbr  14467  1lgs  14740  lgs1  14741  bj-charfun  14855  bj-findis  15027