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  618  mpjaodan  806  mpd3an3  1375  eueq2dc  2993  csbiegf  3185  difsnb  3842  reusv3i  4585  fimadmfo  5604  fvmpt3  5761  ffvelcdmd  5818  fnressn  5875  fliftel1  5973  f1oiso2  6006  riota5f  6038  1stvalg  6349  2ndvalg  6350  brtpos2  6495  tfrlemibxssdm  6571  dom2lem  7024  php5  7125  nnfi  7140  xpfi  7205  supisoti  7314  ordiso2  7339  omp1eomlem  7398  nnnninfeq2  7433  onenon  7493  oncardval  7495  cardonle  7496  recidnq  7724  archnqq  7748  prarloclemarch2  7750  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  recexprlemex  7968  0idsr  8098  lep1  9139  suprlubex  9246  uz11  9898  xnegid  10214  eluzfz2  10389  fzsuc  10427  fzsuc2  10438  fzp1disj  10439  fzneuz  10460  fzp1nel  10463  nn0p1elfzo  10546  exbtwnzlemex  10636  flhalf  10689  modqval  10713  frec2uzsucd  10790  frecuzrdgsuc  10803  uzsinds  10833  seq3p1  10854  seqp1cd  10859  expubnd  10985  iexpcyc  11033  binom2sub1  11043  hashennn  11171  lswwrd  11299  eqs1  11344  pfxid  11406  wrdind  11442  wrd2ind  11443  pfxccatpfx2  11457  swrdccat3blem  11459  shftfval  11534  shftcan1  11547  cjval  11558  reval  11562  imval  11563  cjmulrcl  11600  addcj  11604  absval  11714  resqrexlemdecn  11725  resqrexlemnmsq  11730  resqrexlemnm  11731  absneg  11763  abscj  11765  sqabsadd  11768  sqabssub  11769  ltabs  11800  dfabsmax  11930  negfi  11941  fsum3  12101  trirecip  12215  fprodseq  12297  efval  12375  ege2le3  12385  efcan  12390  sinval  12416  cosval  12417  efi4p  12431  resin4p  12432  recos4p  12433  sincossq  12462  eirraplem  12491  iddvds  12518  1dvds  12519  bezoutlemstep  12721  coprmgcdb  12813  1idssfct  12840  exprmfct  12863  oddpwdclemdc  12898  phival  12938  odzphi  12972  oddprmdvds  13080  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemsi  13205  ballotfilemfrci  13218  setsn0fun  13336  gsumfzval  13657  0subm  13742  gsumfzz  13753  grprcan  13795  isgrpid2  13798  grpinvid  13818  mulgval  13878  mulgnn0z  13905  0subg  13955  qus0  13991  ghmker  14026  imasabl  14092  mgpplusgg  14166  mgpbasg  14168  mgpscag  14169  mgptsetg  14170  mgpdsg  14172  rngen1zr0  14204  srgen1zr0  14234  opprmulfvalg  14316  opprsllem  14320  1unit  14355  1rinv  14376  subrngmcl  14458  subrg1  14480  subrgmcl  14482  subrgdvds  14484  subrguss  14485  subrginv  14486  subrgdv  14487  subrgunit  14488  subrgugrp  14489  rnrhmsubrg  14501  lmodfopne  14603  lsssn0  14647  lspsn0  14699  lsp0  14700  sralmod  14727  2idlval  14779  cnfldneg  14850  zrhval  14894  psrbagfsupp  14948  cldval  15093  ntrfval  15094  clsfval  15095  neifval  15134  tx1cn  15263  ismet  15338  isxmet  15339  divcnap  15559  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  sgmnncl  15985  1lgs  16045  lgs1  16046  uhgredgiedgb  16258  uhgriedg0edg0  16259  subgrprop3  16386  wlklenvm1  16465  wlklenvm1g  16466  wlkl1loop  16482  wlklenvclwlk  16497  umgrclwwlkge2  16526  clwwlknp  16541  bj-charfun  16716  bj-findis  16888