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  2925  csbiegf  3115  difsnb  3750  reusv3i  4477  fvmpt3  5616  ffvelcdmd  5673  fnressn  5723  fliftel1  5816  f1oiso2  5849  riota5f  5877  1stvalg  6168  2ndvalg  6169  brtpos2  6277  tfrlemibxssdm  6353  dom2lem  6799  php5  6887  nnfi  6901  xpfi  6959  supisoti  7040  ordiso2  7065  omp1eomlem  7124  nnnninfeq2  7158  onenon  7214  oncardval  7216  cardonle  7217  recidnq  7423  archnqq  7447  prarloclemarch2  7449  recexprlem1ssl  7663  recexprlem1ssu  7664  recexprlemss1l  7665  recexprlemss1u  7666  recexprlemex  7667  0idsr  7797  lep1  8833  suprlubex  8940  uz11  9582  xnegid  9891  eluzfz2  10064  fzsuc  10101  fzsuc2  10111  fzp1disj  10112  fzneuz  10133  fzp1nel  10136  exbtwnzlemex  10282  flhalf  10335  modqval  10357  frec2uzsucd  10434  frecuzrdgsuc  10447  uzsinds  10475  seq3p1  10495  seqp1cd  10499  expubnd  10611  iexpcyc  10659  binom2sub1  10669  hashennn  10795  shftfval  10865  shftcan1  10878  cjval  10889  reval  10893  imval  10894  cjmulrcl  10931  addcj  10935  absval  11045  resqrexlemdecn  11056  resqrexlemnmsq  11061  resqrexlemnm  11062  absneg  11094  abscj  11096  sqabsadd  11099  sqabssub  11100  ltabs  11131  dfabsmax  11261  negfi  11271  fsum3  11430  trirecip  11544  fprodseq  11626  efval  11704  ege2le3  11714  efcan  11719  sinval  11745  cosval  11746  efi4p  11760  resin4p  11761  recos4p  11762  sincossq  11791  eirraplem  11819  iddvds  11846  1dvds  11847  bezoutlemstep  12033  coprmgcdb  12123  1idssfct  12150  exprmfct  12173  oddpwdclemdc  12208  phival  12248  odzphi  12281  oddprmdvds  12389  setsn0fun  12552  0subm  12951  grprcan  12996  isgrpid2  12999  grpinvid  13019  mulgval  13079  mulgnn0z  13106  0subg  13155  qus0  13191  ghmker  13226  imasabl  13290  mgpplusgg  13295  mgpbasg  13297  mgpscag  13298  mgptsetg  13299  mgpdsg  13301  srgen1zr  13359  opprmulfvalg  13437  opprsllem  13441  1unit  13474  1rinv  13495  subrngmcl  13573  subrg1  13595  subrgmcl  13597  subrgdvds  13599  subrguss  13600  subrginv  13601  subrgdv  13602  subrgunit  13603  subrgugrp  13604  lmodfopne  13659  lsssn0  13703  lspsn0  13755  lsp0  13756  sralmod  13783  cnfldneg  13893  cldval  14076  ntrfval  14077  clsfval  14078  neifval  14117  tx1cn  14246  ismet  14321  isxmet  14322  divcnap  14532  dvaddxxbr  14642  dvmulxxbr  14643  dvcoapbr  14648  1lgs  14922  lgs1  14923  bj-charfun  15037  bj-findis  15209