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  7274  djuen  7294  dftap2  7334  2omotaplemst  7341  exmidapne  7343  ccfunen  7347  dfplpq2  7438  ltbtwnnqq  7499  enq0tr  7518  elnp1st2nd  7560  prcdnql  7568  prnminu  7573  prloc  7575  genpcdl  7603  addnqprulem  7612  addlocprlemlt  7615  addlocprlemgt  7618  addlocprlem  7619  addlocpr  7620  nqprxx  7630  ltnqex  7633  addnqprlemfl  7643  addnqprlemfu  7644  appdivnq  7647  prmuloclemcalc  7649  prmuloc  7650  mullocprlem  7654  mulnqprlemfl  7659  mulnqprlemfu  7660  ltprordil  7673  ltnqpri  7678  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  ltexpri  7697  lteupri  7701  ltaprlem  7702  recexprlemell  7706  recexprlemelu  7707  recexprlemloc  7715  recexprlempr  7716  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1u  7720  aptipr  7725  cauappcvgprlemm  7729  cauappcvgprlemlol  7731  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlem1  7743  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemlol  7754  caucvgprlemladdfu  7761  caucvgprprlemloccalc  7768  caucvgprprlemnkltj  7773  caucvgprprlemnbj  7777  caucvgprprlemml  7778  caucvgprprlemlol  7782  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  suplocexprlemss  7799  suplocexprlemru  7803  suplocexprlemlub  7808  ltsrprg  7831  caucvgsrlemasr  7874  suplocsrlemb  7890  suplocsrlem  7892  suplocsr  7893  axcaucvglemcau  7982  axpre-suploclemres  7985  negf1o  8425  apreap  8631  apreim  8647  msqge0  8660  mulge0  8663  apti  8666  apsscn  8691  mulap0bad  8703  divadddivap  8771  recnz  9436  lbzbi  9707  xadd4d  9977  ixxss1  9996  ixxss2  9997  ixxss12  9998  iccss2  10036  iccssioo2  10038  iccssico2  10039  iccen  10098  elfzole1  10248  ioom  10367  elicore  10373  flqle  10385  flqltnz  10394  addmodlteq  10507  expclzap  10673  hashennnuni  10888  zfz1isolem1  10949  recl  11035  cvg1nlemcau  11166  cvg1nlemres  11167  resqrtth  11213  fimaxre2  11409  climcl  11464  reccn2ap  11495  nnf1o  11558  summodclem3  11562  sumpr  11595  fsump1i  11615  fisumcom2  11620  fsum00  11644  fsumparts  11652  mertenslemi1  11717  prodmodclem3  11757  fprodcom2fi  11808  addsin  11924  subsin  11925  addcos  11928  subcos  11929  sinbnd2  11936  cosbnd2  11937  sin01gt0  11944  cos01gt0  11945  divgcdz  12163  divgcdnn  12167  gcdaddm  12176  bezoutlemstep  12189  dvdsgcdb  12205  dfgcd2  12206  mulgcd  12208  gcdzeq  12214  dvdsmulgcd  12217  sqgcd  12221  bezoutr  12224  lcmval  12256  lcmcllem  12260  gcddvdslcm  12266  lcmgcdlem  12270  lcmgcd  12271  lcmgcdeq  12276  lcmdvdsb  12277  mulgcddvds  12287  rpmulgcd2  12288  qredeu  12290  rpdvds  12292  isprm3  12311  divgcdodd  12336  coprm  12337  rpexp  12346  sqrt2irr  12355  qnumcl  12381  qnumdencoprm  12386  divnumden  12389  numsq  12396  phimullem  12418  eulerthlem1  12420  prmdiveq  12429  prmdivdiv  12430  hashgcdlem  12431  odzcl  12437  reumodprminv  12447  pythagtriplem19  12476  pclemub  12481  pcprendvds  12484  pcprendvds2  12485  pcpre1  12486  pcpremul  12487  pceulem  12488  pceu  12489  pczpre  12491  pczcl  12492  pcgcd1  12522  pc2dvds  12524  pcaddlem  12533  pcmpt  12537  pockthlem  12550  prmunb  12556  4sqlem7  12578  4sqlem8  12579  4sqlem9  12580  4sqlem10  12581  4sqlem14  12598  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  4sqlem18  12602  ennnfonelemg  12645  ennnfonelemf1  12660  ctiunctlemu1st  12676  nninfdclemf  12691  nninfdclemp1  12692  mgmidcl  13080  gsumfzval  13093  gsumval2  13099  mndlid  13137  prdsmndd  13150  imasmndf1  13156  dfgrp3mlem  13300  grplactf1o  13305  prdsgrpd  13311  prdsinvgd  13312  imasgrpf1  13318  subgsubm  13402  qusgrp  13438  ghmgrp1  13451  ghmf  13453  ghmnsgpreima  13475  kerf1ghm  13480  conjsubg  13483  imasrng  13588  srgdilem  13601  srgdi  13606  srglidm  13611  ringdilem  13644  ringdi  13650  ringlidm  13655  imasring  13696  imasringf1  13697  dvdsrcld  13729  unitcld  13740  unitmulcl  13745  unitnegcl  13762  rhmghm  13794  elrhmunit  13809  subrgss  13854  subrgrcl  13858  lmodvscl  13937  lmodvsdi  13943  lmodvsdir  13944  lsslsp  14061  qusring  14159  crngridl  14162  znunit  14291  znrrg  14292  psrbaglesuppg  14302  psrelbas  14304  psraddcl  14308  uniopn  14321  restbasg  14488  cntop1  14521  cnf  14524  cnpf2  14527  lmtopcnp  14570  psmetdmdm  14644  psmetf  14645  psmet0  14647  xmetf  14670  metf  14671  blhalf  14728  xmetxpbl  14828  ioo2bl  14871  tgioo  14874  cncff  14897  rescncf  14901  cdivcncfap  14924  cnopnap  14931  divcncfap  14934  dedekindeulemeu  14942  dedekindicclemeu  14951  ivthinclemlm  14954  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthinclemdisj  14960  ivthdec  14964  ivthreinc  14965  limcimolemlt  14984  limcimo  14985  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  limccoap  14998  eldvap  15002  dvbsssg  15006  dvfgg  15008  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcj  15029  dvfre  15030  dvrecap  15033  plyco  15079  plycj  15081  sin0pilem1  15101  sin0pilem2  15102  pilem3  15103  tanrpcl  15157  tangtx  15158  perfect  15321  lgsne0  15363  lgseisen  15399  lgsquad2lem2  15407  2sqlem8a  15447  2sqlem8  15448  nninfalllem1  15739  iooref1o  15765  alsi1d  15812  alsc1d  15814