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  simprld  530  simp1  999  eldifad  3168  unssad  3341  opth1  4270  opth  4271  0nelop  4282  epelg  4326  poirr  4343  brrelex1  4703  brrelex  4704  asymref  5056  soirri  5065  sotri  5066  fcnvres  5444  fun11iun  5528  elmpocl1  6123  f1od  6130  f1o2d  6132  oprssdmm  6238  smoiso  6369  tfrlem1  6375  swoer  6629  ecopovtrn  6700  ecopovtrng  6703  elmapssres  6741  pmresg  6744  mapsspm  6750  en1uniel  6872  pw2f1odc  6905  xpf1o  6914  sbthlemi9  7040  supelti  7077  supsnti  7080  supisoti  7085  ctssdccl  7186  ctfoex  7193  fodjum  7221  en2eleq  7276  djuen  7296  dftap2  7336  2omotaplemst  7343  exmidapne  7345  ccfunen  7349  dfplpq2  7440  ltbtwnnqq  7501  enq0tr  7520  elnp1st2nd  7562  prcdnql  7570  prnminu  7575  prloc  7577  genpcdl  7605  addnqprulem  7614  addlocprlemlt  7617  addlocprlemgt  7620  addlocprlem  7621  addlocpr  7622  nqprxx  7632  ltnqex  7635  addnqprlemfl  7645  addnqprlemfu  7646  appdivnq  7649  prmuloclemcalc  7651  prmuloc  7652  mullocprlem  7656  mulnqprlemfl  7661  mulnqprlemfu  7662  ltprordil  7675  ltnqpri  7680  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltexpri  7699  lteupri  7703  ltaprlem  7704  recexprlemell  7708  recexprlemelu  7709  recexprlemloc  7717  recexprlempr  7718  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1u  7722  aptipr  7727  cauappcvgprlemm  7731  cauappcvgprlemlol  7733  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlem1  7745  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemlol  7756  caucvgprlemladdfu  7763  caucvgprprlemloccalc  7770  caucvgprprlemnkltj  7775  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemlol  7784  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  suplocexprlemss  7801  suplocexprlemru  7805  suplocexprlemlub  7810  ltsrprg  7833  caucvgsrlemasr  7876  suplocsrlemb  7892  suplocsrlem  7894  suplocsr  7895  axcaucvglemcau  7984  axpre-suploclemres  7987  negf1o  8427  apreap  8633  apreim  8649  msqge0  8662  mulge0  8665  apti  8668  apsscn  8693  mulap0bad  8705  divadddivap  8773  recnz  9438  lbzbi  9709  xadd4d  9979  ixxss1  9998  ixxss2  9999  ixxss12  10000  iccss2  10038  iccssioo2  10040  iccssico2  10041  iccen  10100  elfzole1  10250  ioom  10369  elicore  10375  flqle  10387  flqltnz  10396  addmodlteq  10509  expclzap  10675  hashennnuni  10890  zfz1isolem1  10951  recl  11037  cvg1nlemcau  11168  cvg1nlemres  11169  resqrtth  11215  fimaxre2  11411  climcl  11466  reccn2ap  11497  nnf1o  11560  summodclem3  11564  sumpr  11597  fsump1i  11617  fisumcom2  11622  fsum00  11646  fsumparts  11654  mertenslemi1  11719  prodmodclem3  11759  fprodcom2fi  11810  addsin  11926  subsin  11927  addcos  11930  subcos  11931  sinbnd2  11938  cosbnd2  11939  sin01gt0  11946  cos01gt0  11947  divgcdz  12165  divgcdnn  12169  gcdaddm  12178  bezoutlemstep  12191  dvdsgcdb  12207  dfgcd2  12208  mulgcd  12210  gcdzeq  12216  dvdsmulgcd  12219  sqgcd  12223  bezoutr  12226  lcmval  12258  lcmcllem  12262  gcddvdslcm  12268  lcmgcdlem  12272  lcmgcd  12273  lcmgcdeq  12278  lcmdvdsb  12279  mulgcddvds  12289  rpmulgcd2  12290  qredeu  12292  rpdvds  12294  isprm3  12313  divgcdodd  12338  coprm  12339  rpexp  12348  sqrt2irr  12357  qnumcl  12383  qnumdencoprm  12388  divnumden  12391  numsq  12398  phimullem  12420  eulerthlem1  12422  prmdiveq  12431  prmdivdiv  12432  hashgcdlem  12433  odzcl  12439  reumodprminv  12449  pythagtriplem19  12478  pclemub  12483  pcprendvds  12486  pcprendvds2  12487  pcpre1  12488  pcpremul  12489  pceulem  12490  pceu  12491  pczpre  12493  pczcl  12494  pcgcd1  12524  pc2dvds  12526  pcaddlem  12535  pcmpt  12539  pockthlem  12552  prmunb  12558  4sqlem7  12580  4sqlem8  12581  4sqlem9  12582  4sqlem10  12583  4sqlem14  12600  4sqlem15  12601  4sqlem16  12602  4sqlem17  12603  4sqlem18  12604  ennnfonelemg  12647  ennnfonelemf1  12662  ctiunctlemu1st  12678  nninfdclemf  12693  nninfdclemp1  12694  mgmidcl  13082  gsumfzval  13095  gsumval2  13101  mndlid  13139  prdsmndd  13152  imasmndf1  13158  dfgrp3mlem  13302  grplactf1o  13307  prdsgrpd  13313  prdsinvgd  13314  imasgrpf1  13320  subgsubm  13404  qusgrp  13440  ghmgrp1  13453  ghmf  13455  ghmnsgpreima  13477  kerf1ghm  13482  conjsubg  13485  imasrng  13590  srgdilem  13603  srgdi  13608  srglidm  13613  ringdilem  13646  ringdi  13652  ringlidm  13657  imasring  13698  imasringf1  13699  dvdsrcld  13731  unitcld  13742  unitmulcl  13747  unitnegcl  13764  rhmghm  13796  elrhmunit  13811  subrgss  13856  subrgrcl  13860  lmodvscl  13939  lmodvsdi  13945  lmodvsdir  13946  lsslsp  14063  qusring  14161  crngridl  14164  znunit  14293  znrrg  14294  psrbaglesuppg  14306  psrelbas  14309  psraddcl  14314  mplrcl  14328  uniopn  14345  restbasg  14512  cntop1  14545  cnf  14548  cnpf2  14551  lmtopcnp  14594  psmetdmdm  14668  psmetf  14669  psmet0  14671  xmetf  14694  metf  14695  blhalf  14752  xmetxpbl  14852  ioo2bl  14895  tgioo  14898  cncff  14921  rescncf  14925  cdivcncfap  14948  cnopnap  14955  divcncfap  14958  dedekindeulemeu  14966  dedekindicclemeu  14975  ivthinclemlm  14978  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthinclemdisj  14984  ivthdec  14988  ivthreinc  14989  limcimolemlt  15008  limcimo  15009  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  limccoap  15022  eldvap  15026  dvbsssg  15030  dvfgg  15032  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcj  15053  dvfre  15054  dvrecap  15057  plyco  15103  plycj  15105  sin0pilem1  15125  sin0pilem2  15126  pilem3  15127  tanrpcl  15181  tangtx  15182  perfect  15345  lgsne0  15387  lgseisen  15423  lgsquad2lem2  15431  2sqlem8a  15471  2sqlem8  15472  nninfalllem1  15763  iooref1o  15791  alsi1d  15838  alsc1d  15840