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  4474  fvmpt3  5612  ffvelcdmd  5669  fnressn  5719  fliftel1  5812  f1oiso2  5845  riota5f  5872  1stvalg  6162  2ndvalg  6163  brtpos2  6271  tfrlemibxssdm  6347  dom2lem  6791  php5  6877  nnfi  6891  xpfi  6948  supisoti  7029  ordiso2  7054  omp1eomlem  7113  nnnninfeq2  7147  onenon  7203  oncardval  7205  cardonle  7206  recidnq  7412  archnqq  7436  prarloclemarch2  7438  recexprlem1ssl  7652  recexprlem1ssu  7653  recexprlemss1l  7654  recexprlemss1u  7655  recexprlemex  7656  0idsr  7786  lep1  8822  suprlubex  8929  uz11  9570  xnegid  9879  eluzfz2  10052  fzsuc  10089  fzsuc2  10099  fzp1disj  10100  fzneuz  10121  fzp1nel  10124  exbtwnzlemex  10270  flhalf  10322  modqval  10344  frec2uzsucd  10421  frecuzrdgsuc  10434  uzsinds  10462  seq3p1  10482  seqp1cd  10486  expubnd  10597  iexpcyc  10645  binom2sub1  10655  hashennn  10780  shftfval  10850  shftcan1  10863  cjval  10874  reval  10878  imval  10879  cjmulrcl  10916  addcj  10920  absval  11030  resqrexlemdecn  11041  resqrexlemnmsq  11046  resqrexlemnm  11047  absneg  11079  abscj  11081  sqabsadd  11084  sqabssub  11085  ltabs  11116  dfabsmax  11246  negfi  11256  fsum3  11415  trirecip  11529  fprodseq  11611  efval  11689  ege2le3  11699  efcan  11704  sinval  11730  cosval  11731  efi4p  11745  resin4p  11746  recos4p  11747  sincossq  11776  eirraplem  11804  iddvds  11831  1dvds  11832  bezoutlemstep  12018  coprmgcdb  12108  1idssfct  12135  exprmfct  12158  oddpwdclemdc  12193  phival  12233  odzphi  12266  oddprmdvds  12372  setsn0fun  12524  0subm  12909  grprcan  12954  isgrpid2  12957  grpinvid  12977  mulgval  13037  mulgnn0z  13062  0subg  13111  ghmker  13177  imasabl  13241  mgpplusgg  13246  mgpbasg  13248  mgpscag  13249  mgptsetg  13250  mgpdsg  13252  srgen1zr  13310  opprmulfvalg  13388  opprsllem  13392  1unit  13425  1rinv  13446  subrngmcl  13524  subrg1  13546  subrgmcl  13548  subrgdvds  13550  subrguss  13551  subrginv  13552  subrgdv  13553  subrgunit  13554  subrgugrp  13555  lmodfopne  13610  lsssn0  13654  lspsn0  13706  lsp0  13707  sralmod  13734  cnfldneg  13844  cldval  14003  ntrfval  14004  clsfval  14005  neifval  14044  tx1cn  14173  ismet  14248  isxmet  14249  divcnap  14459  dvaddxxbr  14569  dvmulxxbr  14570  dvcoapbr  14575  1lgs  14848  lgs1  14849  bj-charfun  14963  bj-findis  15135