Theorem simpld 112

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
simpld.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simpld	⊢ (𝜑 → 𝜓)

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is referenced by:  biimp  118  simplbi  274  simprbda  383  simplld  528  simplrd  530  simprld  532  simp1  1024  eldifad  3212  unssad  3386  opth1  4334  opth  4335  0nelop  4346  epelg  4393  poirr  4410  brrelex1  4771  brrelex  4772  asymref  5129  soirri  5138  sotri  5139  ffdmd  5514  fcnvres  5528  fun11iun  5613  funopsn  5838  elmpocl1  6228  f1od  6236  f1o2d  6238  oprssdmm  6343  elmpom  6412  fczsupp0  6437  smoiso  6511  tfrlem1  6517  swoer  6773  ecopovtrn  6844  ecopovtrng  6847  elmapssres  6885  pmresg  6888  mapsspm  6894  en1uniel  7021  pw2f1odc  7064  xpf1o  7073  sbthlemi9  7207  supelti  7244  supsnti  7247  supisoti  7252  ctssdccl  7353  ctfoex  7360  fodjum  7388  en2eleq  7449  djuen  7469  pw1if  7486  dftap2  7513  2omotaplemst  7520  exmidapne  7522  ccfunen  7526  dfplpq2  7617  ltbtwnnqq  7678  enq0tr  7697  elnp1st2nd  7739  prcdnql  7747  prnminu  7752  prloc  7754  genpcdl  7782  addnqprulem  7791  addlocprlemlt  7794  addlocprlemgt  7797  addlocprlem  7798  addlocpr  7799  nqprxx  7809  ltnqex  7812  addnqprlemfl  7822  addnqprlemfu  7823  appdivnq  7826  prmuloclemcalc  7828  prmuloc  7829  mullocprlem  7833  mulnqprlemfl  7838  mulnqprlemfu  7839  ltprordil  7852  ltnqpri  7857  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  ltexpri  7876  lteupri  7880  ltaprlem  7881  recexprlemell  7885  recexprlemelu  7886  recexprlemloc  7894  recexprlempr  7895  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1u  7899  aptipr  7904  cauappcvgprlemm  7908  cauappcvgprlemlol  7910  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlem1  7922  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemlol  7933  caucvgprlemladdfu  7940  caucvgprprlemloccalc  7947  caucvgprprlemnkltj  7952  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemlol  7961  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  suplocexprlemss  7978  suplocexprlemru  7982  suplocexprlemlub  7987  ltsrprg  8010  caucvgsrlemasr  8053  suplocsrlemb  8069  suplocsrlem  8071  suplocsr  8072  axcaucvglemcau  8161  axpre-suploclemres  8164  negf1o  8604  apreap  8810  apreim  8826  msqge0  8839  mulge0  8842  apti  8845  apsscn  8870  mulap0bad  8882  divadddivap  8950  recnz  9616  lbzbi  9893  xadd4d  10163  ixxss1  10182  ixxss2  10183  ixxss12  10184  iccss2  10222  iccssioo2  10224  iccssico2  10225  iccen  10284  elfzole1  10434  ioom  10564  elicore  10570  flqle  10582  flqltnz  10591  addmodlteq  10704  expclzap  10870  hashennnuni  11085  zfz1isolem1  11148  hashdmprop2dom  11152  swrdsbslen  11294  ccatswrd  11298  ccatpfx  11329  recl  11474  cvg1nlemcau  11605  cvg1nlemres  11606  resqrtth  11652  fimaxre2  11848  climcl  11903  reccn2ap  11934  nnf1o  11998  summodclem3  12002  sumpr  12035  fsump1i  12055  fisumcom2  12060  fsum00  12084  fsumparts  12092  mertenslemi1  12157  prodmodclem3  12197  fprodcom2fi  12248  addsin  12364  subsin  12365  addcos  12368  subcos  12369  sinbnd2  12376  cosbnd2  12377  sin01gt0  12384  cos01gt0  12385  divgcdz  12603  divgcdnn  12607  gcdaddm  12616  bezoutlemstep  12629  dvdsgcdb  12645  dfgcd2  12646  mulgcd  12648  gcdzeq  12654  dvdsmulgcd  12657  sqgcd  12661  bezoutr  12664  lcmval  12696  lcmcllem  12700  gcddvdslcm  12706  lcmgcdlem  12710  lcmgcd  12711  lcmgcdeq  12716  lcmdvdsb  12717  mulgcddvds  12727  rpmulgcd2  12728  qredeu  12730  rpdvds  12732  isprm3  12751  divgcdodd  12776  coprm  12777  rpexp  12786  sqrt2irr  12795  qnumcl  12821  qnumdencoprm  12826  divnumden  12829  numsq  12836  phimullem  12858  eulerthlem1  12860  prmdiveq  12869  prmdivdiv  12870  hashgcdlem  12871  odzcl  12877  reumodprminv  12887  pythagtriplem19  12916  pclemub  12921  pcprendvds  12924  pcprendvds2  12925  pcpre1  12926  pcpremul  12927  pceulem  12928  pceu  12929  pczpre  12931  pczcl  12932  pcgcd1  12962  pc2dvds  12964  pcaddlem  12973  pcmpt  12977  pockthlem  12990  prmunb  12996  4sqlem7  13018  4sqlem8  13019  4sqlem9  13020  4sqlem10  13021  4sqlem14  13038  4sqlem15  13039  4sqlem16  13040  4sqlem17  13041  4sqlem18  13042  ennnfonelemg  13085  ennnfonelemf1  13100  ctiunctlemu1st  13116  nninfdclemf  13131  nninfdclemp1  13132  mgmidcl  13522  gsumfzval  13535  gsumval2  13541  mndlid  13579  prdsmndd  13592  imasmndf1  13598  dfgrp3mlem  13742  grplactf1o  13747  prdsgrpd  13753  prdsinvgd  13754  imasgrpf1  13760  subgsubm  13844  qusgrp  13880  ghmgrp1  13893  ghmf  13895  ghmnsgpreima  13917  kerf1ghm  13922  conjsubg  13925  gsumsplit0  13994  imasrng  14031  srgdilem  14044  srgdi  14049  srglidm  14054  ringdilem  14087  ringdi  14093  ringlidm  14098  imasring  14139  imasringf1  14140  dvdsrcld  14173  unitcld  14184  unitmulcl  14189  unitnegcl  14206  rhmghm  14238  elrhmunit  14253  subrgss  14298  subrgrcl  14302  lmodvscl  14381  lmodvsdi  14387  lmodvsdir  14388  lsslsp  14505  qusring  14603  crngridl  14606  znunit  14735  znrrg  14736  psrbaglesuppg  14748  psrbagcon  14752  psrbagconcl  14753  psrelbas  14756  psraddcl  14761  mplrcl  14775  uniopn  14792  restbasg  14959  cntop1  14992  cnf  14995  cnpf2  14998  lmtopcnp  15041  psmetdmdm  15115  psmetf  15116  psmet0  15118  xmetf  15141  metf  15142  blhalf  15199  xmetxpbl  15299  ioo2bl  15342  tgioo  15345  cncff  15368  rescncf  15372  cdivcncfap  15395  cnopnap  15402  divcncfap  15405  dedekindeulemeu  15413  dedekindicclemeu  15422  ivthinclemlm  15425  ivthinclemlopn  15427  ivthinclemuopn  15429  ivthinclemdisj  15431  ivthdec  15435  ivthreinc  15436  limcimolemlt  15455  limcimo  15456  limccnpcntop  15466  limccnp2lem  15467  limccnp2cntop  15468  limccoap  15469  eldvap  15473  dvbsssg  15477  dvfgg  15479  dvaddxxbr  15492  dvmulxxbr  15493  dvcoapbr  15498  dvcj  15500  dvfre  15501  dvrecap  15504  plyco  15550  plycj  15552  sin0pilem1  15572  sin0pilem2  15573  pilem3  15574  tanrpcl  15628  tangtx  15629  perfect  15795  lgsne0  15837  lgseisen  15873  lgsquad2lem2  15881  2sqlem8a  15921  2sqlem8  15922  structgrssvtx  15963  edguhgr  16058  umgrpredgv  16068  umgrnloop2  16072  umgr2edg  16128  subuhgr  16193  subumgr  16195  subusgr  16196  wlkpropg  16245  wlkv  16247  wlkvtxeledgg  16265  wlkvtxiedgg  16267  wlk1walkdom  16280  trlsv  16305  clwwlksswrd  16318  clwwlkclwwlkn  16330  eupthv  16367  eupthseg  16373  eupth2lem3lem3fi  16391  eupth2lem3lem4fi  16394  eupth2lemsfi  16399  eulerpathprum  16401  nninfalllem1  16714  iooref1o  16746  gfsumval  16789  alsi1d  16804  alsc1d  16806