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  2937  csbiegf  3128  difsnb  3766  reusv3i  4495  fimadmfo  5492  fvmpt3  5643  ffvelcdmd  5701  fnressn  5751  fliftel1  5844  f1oiso2  5877  riota5f  5905  1stvalg  6209  2ndvalg  6210  brtpos2  6318  tfrlemibxssdm  6394  dom2lem  6840  php5  6928  nnfi  6942  xpfi  7002  supisoti  7085  ordiso2  7110  omp1eomlem  7169  nnnninfeq2  7204  onenon  7264  oncardval  7266  cardonle  7267  recidnq  7479  archnqq  7503  prarloclemarch2  7505  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  recexprlemex  7723  0idsr  7853  lep1  8891  suprlubex  8998  uz11  9643  xnegid  9953  eluzfz2  10126  fzsuc  10163  fzsuc2  10173  fzp1disj  10174  fzneuz  10195  fzp1nel  10198  exbtwnzlemex  10358  flhalf  10411  modqval  10435  frec2uzsucd  10512  frecuzrdgsuc  10525  uzsinds  10555  seq3p1  10576  seqp1cd  10581  expubnd  10707  iexpcyc  10755  binom2sub1  10765  hashennn  10891  shftfval  11005  shftcan1  11018  cjval  11029  reval  11033  imval  11034  cjmulrcl  11071  addcj  11075  absval  11185  resqrexlemdecn  11196  resqrexlemnmsq  11201  resqrexlemnm  11202  absneg  11234  abscj  11236  sqabsadd  11239  sqabssub  11240  ltabs  11271  dfabsmax  11401  negfi  11412  fsum3  11571  trirecip  11685  fprodseq  11767  efval  11845  ege2le3  11855  efcan  11860  sinval  11886  cosval  11887  efi4p  11901  resin4p  11902  recos4p  11903  sincossq  11932  eirraplem  11961  iddvds  11988  1dvds  11989  bezoutlemstep  12191  coprmgcdb  12283  1idssfct  12310  exprmfct  12333  oddpwdclemdc  12368  phival  12408  odzphi  12442  oddprmdvds  12550  setsn0fun  12742  gsumfzval  13095  0subm  13188  gsumfzz  13199  grprcan  13241  isgrpid2  13244  grpinvid  13264  mulgval  13330  mulgnn0z  13357  0subg  13407  qus0  13443  ghmker  13478  imasabl  13544  mgpplusgg  13558  mgpbasg  13560  mgpscag  13561  mgptsetg  13562  mgpdsg  13564  srgen1zr  13622  opprmulfvalg  13704  opprsllem  13708  1unit  13741  1rinv  13762  subrngmcl  13843  subrg1  13865  subrgmcl  13867  subrgdvds  13869  subrguss  13870  subrginv  13871  subrgdv  13872  subrgunit  13873  subrgugrp  13874  rnrhmsubrg  13886  lmodfopne  13960  lsssn0  14004  lspsn0  14056  lsp0  14057  sralmod  14084  2idlval  14136  cnfldneg  14207  zrhval  14251  cldval  14421  ntrfval  14422  clsfval  14423  neifval  14462  tx1cn  14591  ismet  14666  isxmet  14667  divcnap  14887  dvaddxxbr  15023  dvmulxxbr  15024  dvcoapbr  15029  sgmnncl  15310  1lgs  15370  lgs1  15371  bj-charfun  15539  bj-findis  15711