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  mpjaodan  798  mpd3an3  1338  eueq2dc  2912  csbiegf  3102  difsnb  3737  reusv3i  4461  fvmpt3  5597  ffvelcdmd  5654  fnressn  5704  fliftel1  5797  f1oiso2  5830  riota5f  5857  1stvalg  6145  2ndvalg  6146  brtpos2  6254  tfrlemibxssdm  6330  dom2lem  6774  php5  6860  nnfi  6874  xpfi  6931  supisoti  7011  ordiso2  7036  omp1eomlem  7095  nnnninfeq2  7129  onenon  7185  oncardval  7187  cardonle  7188  recidnq  7394  archnqq  7418  prarloclemarch2  7420  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  recexprlemex  7638  0idsr  7768  lep1  8804  suprlubex  8911  uz11  9552  xnegid  9861  eluzfz2  10034  fzsuc  10071  fzsuc2  10081  fzp1disj  10082  fzneuz  10103  fzp1nel  10106  exbtwnzlemex  10252  flhalf  10304  modqval  10326  frec2uzsucd  10403  frecuzrdgsuc  10416  uzsinds  10444  seq3p1  10464  seqp1cd  10468  expubnd  10579  iexpcyc  10627  binom2sub1  10637  hashennn  10762  shftfval  10832  shftcan1  10845  cjval  10856  reval  10860  imval  10861  cjmulrcl  10898  addcj  10902  absval  11012  resqrexlemdecn  11023  resqrexlemnmsq  11028  resqrexlemnm  11029  absneg  11061  abscj  11063  sqabsadd  11066  sqabssub  11067  ltabs  11098  dfabsmax  11228  negfi  11238  fsum3  11397  trirecip  11511  fprodseq  11593  efval  11671  ege2le3  11681  efcan  11686  sinval  11712  cosval  11713  efi4p  11727  resin4p  11728  recos4p  11729  sincossq  11758  eirraplem  11786  iddvds  11813  1dvds  11814  bezoutlemstep  12000  coprmgcdb  12090  1idssfct  12117  exprmfct  12140  oddpwdclemdc  12175  phival  12215  odzphi  12248  oddprmdvds  12354  setsn0fun  12501  0subm  12876  grprcan  12915  isgrpid2  12918  grpinvid  12935  mulgval  12991  mulgnn0z  13015  0subg  13064  mgpplusgg  13139  mgpbasg  13141  mgpscag  13142  mgptsetg  13143  mgpdsg  13145  srgen1zr  13176  opprmulfvalg  13247  opprsllem  13251  1unit  13281  1rinv  13302  subrg1  13357  subrgmcl  13359  subrgdvds  13361  subrguss  13362  subrginv  13363  subrgdv  13364  subrgunit  13365  subrgugrp  13366  lmodfopne  13421  lsssn0  13461  cnfldneg  13506  cldval  13638  ntrfval  13639  clsfval  13640  neifval  13679  tx1cn  13808  ismet  13883  isxmet  13884  divcnap  14094  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  1lgs  14483  lgs1  14484  bj-charfun  14598  bj-findis  14770