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  2937  csbiegf  3128  difsnb  3766  reusv3i  4495  fimadmfo  5492  fvmpt3  5643  ffvelcdmd  5701  fnressn  5751  fliftel1  5844  f1oiso2  5877  riota5f  5905  1stvalg  6209  2ndvalg  6210  brtpos2  6318  tfrlemibxssdm  6394  dom2lem  6840  php5  6928  nnfi  6942  xpfi  7002  supisoti  7085  ordiso2  7110  omp1eomlem  7169  nnnninfeq2  7204  onenon  7262  oncardval  7264  cardonle  7265  recidnq  7477  archnqq  7501  prarloclemarch2  7503  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  recexprlemex  7721  0idsr  7851  lep1  8889  suprlubex  8996  uz11  9641  xnegid  9951  eluzfz2  10124  fzsuc  10161  fzsuc2  10171  fzp1disj  10172  fzneuz  10193  fzp1nel  10196  exbtwnzlemex  10356  flhalf  10409  modqval  10433  frec2uzsucd  10510  frecuzrdgsuc  10523  uzsinds  10553  seq3p1  10574  seqp1cd  10579  expubnd  10705  iexpcyc  10753  binom2sub1  10763  hashennn  10889  shftfval  11003  shftcan1  11016  cjval  11027  reval  11031  imval  11032  cjmulrcl  11069  addcj  11073  absval  11183  resqrexlemdecn  11194  resqrexlemnmsq  11199  resqrexlemnm  11200  absneg  11232  abscj  11234  sqabsadd  11237  sqabssub  11238  ltabs  11269  dfabsmax  11399  negfi  11410  fsum3  11569  trirecip  11683  fprodseq  11765  efval  11843  ege2le3  11853  efcan  11858  sinval  11884  cosval  11885  efi4p  11899  resin4p  11900  recos4p  11901  sincossq  11930  eirraplem  11959  iddvds  11986  1dvds  11987  bezoutlemstep  12189  coprmgcdb  12281  1idssfct  12308  exprmfct  12331  oddpwdclemdc  12366  phival  12406  odzphi  12440  oddprmdvds  12548  setsn0fun  12740  gsumfzval  13093  0subm  13186  gsumfzz  13197  grprcan  13239  isgrpid2  13242  grpinvid  13262  mulgval  13328  mulgnn0z  13355  0subg  13405  qus0  13441  ghmker  13476  imasabl  13542  mgpplusgg  13556  mgpbasg  13558  mgpscag  13559  mgptsetg  13560  mgpdsg  13562  srgen1zr  13620  opprmulfvalg  13702  opprsllem  13706  1unit  13739  1rinv  13760  subrngmcl  13841  subrg1  13863  subrgmcl  13865  subrgdvds  13867  subrguss  13868  subrginv  13869  subrgdv  13870  subrgunit  13871  subrgugrp  13872  rnrhmsubrg  13884  lmodfopne  13958  lsssn0  14002  lspsn0  14054  lsp0  14055  sralmod  14082  2idlval  14134  cnfldneg  14205  zrhval  14249  cldval  14419  ntrfval  14420  clsfval  14421  neifval  14460  tx1cn  14589  ismet  14664  isxmet  14665  divcnap  14885  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  sgmnncl  15308  1lgs  15368  lgs1  15369  bj-charfun  15537  bj-findis  15709