Theorem mpdan 418

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 409	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mpidan  420  mpan2  422  mpjaodan  788  mpd3an3  1328  eueq2dc  2899  csbiegf  3088  difsnb  3716  reusv3i  4437  fvmpt3  5565  ffvelrnd  5621  fnressn  5671  fliftel1  5762  f1oiso2  5795  riota5f  5822  1stvalg  6110  2ndvalg  6111  brtpos2  6219  tfrlemibxssdm  6295  dom2lem  6738  php5  6824  nnfi  6838  xpfi  6895  supisoti  6975  ordiso2  7000  omp1eomlem  7059  nnnninfeq2  7093  onenon  7140  oncardval  7142  cardonle  7143  recidnq  7334  archnqq  7358  prarloclemarch2  7360  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  recexprlemex  7578  0idsr  7708  lep1  8740  suprlubex  8847  uz11  9488  xnegid  9795  eluzfz2  9967  fzsuc  10004  fzsuc2  10014  fzp1disj  10015  fzneuz  10036  fzp1nel  10039  exbtwnzlemex  10185  flhalf  10237  modqval  10259  frec2uzsucd  10336  frecuzrdgsuc  10349  uzsinds  10377  seq3p1  10397  seqp1cd  10401  expubnd  10512  iexpcyc  10559  binom2sub1  10569  hashennn  10693  shftfval  10763  shftcan1  10776  cjval  10787  reval  10791  imval  10792  cjmulrcl  10829  addcj  10833  absval  10943  resqrexlemdecn  10954  resqrexlemnmsq  10959  resqrexlemnm  10960  absneg  10992  abscj  10994  sqabsadd  10997  sqabssub  10998  ltabs  11029  dfabsmax  11159  negfi  11169  fsum3  11328  trirecip  11442  fprodseq  11524  efval  11602  ege2le3  11612  efcan  11617  sinval  11643  cosval  11644  efi4p  11658  resin4p  11659  recos4p  11660  sincossq  11689  eirraplem  11717  iddvds  11744  1dvds  11745  bezoutlemstep  11930  coprmgcdb  12020  1idssfct  12047  exprmfct  12070  oddpwdclemdc  12105  phival  12145  odzphi  12178  oddprmdvds  12284  setsn0fun  12431  cldval  12739  ntrfval  12740  clsfval  12741  neifval  12780  tx1cn  12909  ismet  12984  isxmet  12985  divcnap  13195  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  1lgs  13584  lgs1  13585  bj-charfun  13689  bj-findis  13861