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  616  mpjaodan  802  mpd3an3  1353  eueq2dc  2956  csbiegf  3148  difsnb  3790  reusv3i  4527  fimadmfo  5533  fvmpt3  5686  ffvelcdmd  5744  fnressn  5798  fliftel1  5891  f1oiso2  5924  riota5f  5954  1stvalg  6258  2ndvalg  6259  brtpos2  6367  tfrlemibxssdm  6443  dom2lem  6893  php5  6987  nnfi  7002  xpfi  7062  supisoti  7145  ordiso2  7170  omp1eomlem  7229  nnnninfeq2  7264  onenon  7324  oncardval  7326  cardonle  7327  recidnq  7548  archnqq  7572  prarloclemarch2  7574  recexprlem1ssl  7788  recexprlem1ssu  7789  recexprlemss1l  7790  recexprlemss1u  7791  recexprlemex  7792  0idsr  7922  lep1  8960  suprlubex  9067  uz11  9713  xnegid  10023  eluzfz2  10196  fzsuc  10233  fzsuc2  10243  fzp1disj  10244  fzneuz  10265  fzp1nel  10268  exbtwnzlemex  10436  flhalf  10489  modqval  10513  frec2uzsucd  10590  frecuzrdgsuc  10603  uzsinds  10633  seq3p1  10654  seqp1cd  10659  expubnd  10785  iexpcyc  10833  binom2sub1  10843  hashennn  10969  lswwrd  11084  eqs1  11127  pfxid  11184  wrdind  11220  wrd2ind  11221  pfxccatpfx2  11235  swrdccat3blem  11237  shftfval  11298  shftcan1  11311  cjval  11322  reval  11326  imval  11327  cjmulrcl  11364  addcj  11368  absval  11478  resqrexlemdecn  11489  resqrexlemnmsq  11494  resqrexlemnm  11495  absneg  11527  abscj  11529  sqabsadd  11532  sqabssub  11533  ltabs  11564  dfabsmax  11694  negfi  11705  fsum3  11864  trirecip  11978  fprodseq  12060  efval  12138  ege2le3  12148  efcan  12153  sinval  12179  cosval  12180  efi4p  12194  resin4p  12195  recos4p  12196  sincossq  12225  eirraplem  12254  iddvds  12281  1dvds  12282  bezoutlemstep  12484  coprmgcdb  12576  1idssfct  12603  exprmfct  12626  oddpwdclemdc  12661  phival  12701  odzphi  12735  oddprmdvds  12843  setsn0fun  13035  gsumfzval  13390  0subm  13483  gsumfzz  13494  grprcan  13536  isgrpid2  13539  grpinvid  13559  mulgval  13625  mulgnn0z  13652  0subg  13702  qus0  13738  ghmker  13773  imasabl  13839  mgpplusgg  13853  mgpbasg  13855  mgpscag  13856  mgptsetg  13857  mgpdsg  13859  srgen1zr  13917  opprmulfvalg  13999  opprsllem  14003  1unit  14036  1rinv  14057  subrngmcl  14138  subrg1  14160  subrgmcl  14162  subrgdvds  14164  subrguss  14165  subrginv  14166  subrgdv  14167  subrgunit  14168  subrgugrp  14169  rnrhmsubrg  14181  lmodfopne  14255  lsssn0  14299  lspsn0  14351  lsp0  14352  sralmod  14379  2idlval  14431  cnfldneg  14502  zrhval  14546  cldval  14738  ntrfval  14739  clsfval  14740  neifval  14779  tx1cn  14908  ismet  14983  isxmet  14984  divcnap  15204  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  sgmnncl  15627  1lgs  15687  lgs1  15688  uhgredgiedgb  15897  uhgriedg0edg0  15898  bj-charfun  16080  bj-findis  16252