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  1021  eldifad  3208  unssad  3381  opth1  4323  opth  4324  0nelop  4335  epelg  4382  poirr  4399  brrelex1  4760  brrelex  4761  asymref  5117  soirri  5126  sotri  5127  ffdmd  5500  fcnvres  5514  fun11iun  5598  funopsn  5822  elmpocl1  6210  f1od  6218  f1o2d  6220  oprssdmm  6326  smoiso  6459  tfrlem1  6465  swoer  6721  ecopovtrn  6792  ecopovtrng  6795  elmapssres  6833  pmresg  6836  mapsspm  6842  en1uniel  6969  pw2f1odc  7009  xpf1o  7018  sbthlemi9  7148  supelti  7185  supsnti  7188  supisoti  7193  ctssdccl  7294  ctfoex  7301  fodjum  7329  en2eleq  7389  djuen  7409  pw1if  7426  dftap2  7453  2omotaplemst  7460  exmidapne  7462  ccfunen  7466  dfplpq2  7557  ltbtwnnqq  7618  enq0tr  7637  elnp1st2nd  7679  prcdnql  7687  prnminu  7692  prloc  7694  genpcdl  7722  addnqprulem  7731  addlocprlemlt  7734  addlocprlemgt  7737  addlocprlem  7738  addlocpr  7739  nqprxx  7749  ltnqex  7752  addnqprlemfl  7762  addnqprlemfu  7763  appdivnq  7766  prmuloclemcalc  7768  prmuloc  7769  mullocprlem  7773  mulnqprlemfl  7778  mulnqprlemfu  7779  ltprordil  7792  ltnqpri  7797  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemlol  7805  ltexprlemopu  7806  ltexprlemupu  7807  ltexprlemdisj  7809  ltexprlemloc  7810  ltexprlemfl  7812  ltexprlemrl  7813  ltexprlemfu  7814  ltexprlemru  7815  ltexpri  7816  lteupri  7820  ltaprlem  7821  recexprlemell  7825  recexprlemelu  7826  recexprlemloc  7834  recexprlempr  7835  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1u  7839  aptipr  7844  cauappcvgprlemm  7848  cauappcvgprlemlol  7850  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdru  7859  cauappcvgprlem1  7862  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemlol  7873  caucvgprlemladdfu  7880  caucvgprprlemloccalc  7887  caucvgprprlemnkltj  7892  caucvgprprlemnbj  7896  caucvgprprlemml  7897  caucvgprprlemlol  7901  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  suplocexprlemss  7918  suplocexprlemru  7922  suplocexprlemlub  7927  ltsrprg  7950  caucvgsrlemasr  7993  suplocsrlemb  8009  suplocsrlem  8011  suplocsr  8012  axcaucvglemcau  8101  axpre-suploclemres  8104  negf1o  8544  apreap  8750  apreim  8766  msqge0  8779  mulge0  8782  apti  8785  apsscn  8810  mulap0bad  8822  divadddivap  8890  recnz  9556  lbzbi  9828  xadd4d  10098  ixxss1  10117  ixxss2  10118  ixxss12  10119  iccss2  10157  iccssioo2  10159  iccssico2  10160  iccen  10219  elfzole1  10369  ioom  10497  elicore  10503  flqle  10515  flqltnz  10524  addmodlteq  10637  expclzap  10803  hashennnuni  11018  zfz1isolem1  11080  hashdmprop2dom  11084  swrdsbslen  11219  ccatswrd  11223  ccatpfx  11254  recl  11385  cvg1nlemcau  11516  cvg1nlemres  11517  resqrtth  11563  fimaxre2  11759  climcl  11814  reccn2ap  11845  nnf1o  11908  summodclem3  11912  sumpr  11945  fsump1i  11965  fisumcom2  11970  fsum00  11994  fsumparts  12002  mertenslemi1  12067  prodmodclem3  12107  fprodcom2fi  12158  addsin  12274  subsin  12275  addcos  12278  subcos  12279  sinbnd2  12286  cosbnd2  12287  sin01gt0  12294  cos01gt0  12295  divgcdz  12513  divgcdnn  12517  gcdaddm  12526  bezoutlemstep  12539  dvdsgcdb  12555  dfgcd2  12556  mulgcd  12558  gcdzeq  12564  dvdsmulgcd  12567  sqgcd  12571  bezoutr  12574  lcmval  12606  lcmcllem  12610  gcddvdslcm  12616  lcmgcdlem  12620  lcmgcd  12621  lcmgcdeq  12626  lcmdvdsb  12627  mulgcddvds  12637  rpmulgcd2  12638  qredeu  12640  rpdvds  12642  isprm3  12661  divgcdodd  12686  coprm  12687  rpexp  12696  sqrt2irr  12705  qnumcl  12731  qnumdencoprm  12736  divnumden  12739  numsq  12746  phimullem  12768  eulerthlem1  12770  prmdiveq  12779  prmdivdiv  12780  hashgcdlem  12781  odzcl  12787  reumodprminv  12797  pythagtriplem19  12826  pclemub  12831  pcprendvds  12834  pcprendvds2  12835  pcpre1  12836  pcpremul  12837  pceulem  12838  pceu  12839  pczpre  12841  pczcl  12842  pcgcd1  12872  pc2dvds  12874  pcaddlem  12883  pcmpt  12887  pockthlem  12900  prmunb  12906  4sqlem7  12928  4sqlem8  12929  4sqlem9  12930  4sqlem10  12931  4sqlem14  12948  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  4sqlem18  12952  ennnfonelemg  12995  ennnfonelemf1  13010  ctiunctlemu1st  13026  nninfdclemf  13041  nninfdclemp1  13042  mgmidcl  13432  gsumfzval  13445  gsumval2  13451  mndlid  13489  prdsmndd  13502  imasmndf1  13508  dfgrp3mlem  13652  grplactf1o  13657  prdsgrpd  13663  prdsinvgd  13664  imasgrpf1  13670  subgsubm  13754  qusgrp  13790  ghmgrp1  13803  ghmf  13805  ghmnsgpreima  13827  kerf1ghm  13832  conjsubg  13835  imasrng  13940  srgdilem  13953  srgdi  13958  srglidm  13963  ringdilem  13996  ringdi  14002  ringlidm  14007  imasring  14048  imasringf1  14049  dvdsrcld  14082  unitcld  14093  unitmulcl  14098  unitnegcl  14115  rhmghm  14147  elrhmunit  14162  subrgss  14207  subrgrcl  14211  lmodvscl  14290  lmodvsdi  14296  lmodvsdir  14297  lsslsp  14414  qusring  14512  crngridl  14515  znunit  14644  znrrg  14645  psrbaglesuppg  14657  psrelbas  14660  psraddcl  14665  mplrcl  14679  uniopn  14696  restbasg  14863  cntop1  14896  cnf  14899  cnpf2  14902  lmtopcnp  14945  psmetdmdm  15019  psmetf  15020  psmet0  15022  xmetf  15045  metf  15046  blhalf  15103  xmetxpbl  15203  ioo2bl  15246  tgioo  15249  cncff  15272  rescncf  15276  cdivcncfap  15299  cnopnap  15306  divcncfap  15309  dedekindeulemeu  15317  dedekindicclemeu  15326  ivthinclemlm  15329  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthinclemdisj  15335  ivthdec  15339  ivthreinc  15340  limcimolemlt  15359  limcimo  15360  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  limccoap  15373  eldvap  15377  dvbsssg  15381  dvfgg  15383  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcj  15404  dvfre  15405  dvrecap  15408  plyco  15454  plycj  15456  sin0pilem1  15476  sin0pilem2  15477  pilem3  15478  tanrpcl  15532  tangtx  15533  perfect  15696  lgsne0  15738  lgseisen  15774  lgsquad2lem2  15782  2sqlem8a  15822  2sqlem8  15823  structgrssvtx  15864  edguhgr  15956  umgrpredgv  15966  umgrnloop2  15970  umgr2edg  16026  wlkpropg  16096  wlkv  16098  wlkvtxeledgg  16116  wlkvtxiedgg  16118  wlk1walkdom  16131  trlsv  16154  clwwlksswrd  16166  clwwlkclwwlkn  16178  nninfalllem1  16488  iooref1o  16516  alsi1d  16563  alsc1d  16565