Theorem mpdan 415

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  mpidan  417  mpan2  419  mpjaodan  770  mpd3an3  1299  eueq2dc  2826  csbiegf  3009  difsnb  3629  reusv3i  4340  fvmpt3  5454  ffvelrnd  5510  fnressn  5560  fliftel1  5649  f1oiso2  5682  riota5f  5708  1stvalg  5994  2ndvalg  5995  brtpos2  6102  tfrlemibxssdm  6178  dom2lem  6620  php5  6705  nnfi  6719  xpfi  6771  supisoti  6849  ordiso2  6872  omp1eomlem  6931  onenon  6990  oncardval  6992  cardonle  6993  recidnq  7149  archnqq  7173  prarloclemarch2  7175  recexprlem1ssl  7389  recexprlem1ssu  7390  recexprlemss1l  7391  recexprlemss1u  7392  recexprlemex  7393  0idsr  7510  lep1  8513  suprlubex  8620  uz11  9250  xnegid  9535  eluzfz2  9705  fzsuc  9742  fzsuc2  9752  fzp1disj  9753  fzneuz  9774  fzp1nel  9777  exbtwnzlemex  9920  flhalf  9968  modqval  9990  frec2uzsucd  10067  frecuzrdgsuc  10080  uzsinds  10108  seq3p1  10128  seqp1cd  10132  expubnd  10243  iexpcyc  10290  binom2sub1  10299  hashennn  10419  shftfval  10486  shftcan1  10499  cjval  10510  reval  10514  imval  10515  cjmulrcl  10552  addcj  10556  absval  10665  resqrexlemdecn  10676  resqrexlemnmsq  10681  resqrexlemnm  10682  absneg  10714  abscj  10716  sqabsadd  10719  sqabssub  10720  ltabs  10751  dfabsmax  10881  negfi  10891  fsum3  11048  trirecip  11162  efval  11218  ege2le3  11228  efcan  11233  sinval  11260  cosval  11261  efi4p  11275  resin4p  11276  recos4p  11277  sincossq  11306  eirraplem  11331  iddvds  11354  1dvds  11355  bezoutlemstep  11531  coprmgcdb  11615  1idssfct  11642  exprmfct  11664  oddpwdclemdc  11696  phival  11734  setsn0fun  11839  cldval  12111  ntrfval  12112  clsfval  12113  neifval  12152  tx1cn  12280  ismet  12333  isxmet  12334  divcnap  12541  dvaddxxbr  12620  dvmulxxbr  12621  bj-findis  12869