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  3221  unssad  3395  opth1  4351  opth  4352  0nelop  4363  epelg  4410  poirr  4427  brrelex1  4788  brrelex  4789  asymref  5147  soirri  5156  sotri  5157  ffdmd  5533  fcnvres  5549  fun11iun  5634  funopsn  5859  elmpocl1  6249  f1od  6257  f1o2d  6259  oprssdmm  6364  elmpom  6433  fczsupp0  6458  smoiso  6532  tfrlem1  6538  swoer  6794  ecopovtrn  6865  ecopovtrng  6868  elmapssres  6906  pmresg  6909  mapsspm  6915  en1uniel  7043  pw2f1odc  7087  xpf1o  7096  sbthlemi9  7234  fsuppfund  7246  supelti  7292  supsnti  7295  supisoti  7300  ctssdccl  7401  ctfoex  7408  fodjum  7436  en2eleq  7497  djuen  7517  pw1if  7534  dftap2  7564  2omotaplemst  7571  exmidapne  7573  ccfunen  7577  dfplpq2  7668  ltbtwnnqq  7729  enq0tr  7748  elnp1st2nd  7790  prcdnql  7798  prnminu  7803  prloc  7805  genpcdl  7833  addnqprulem  7842  addlocprlemlt  7845  addlocprlemgt  7848  addlocprlem  7849  addlocpr  7850  nqprxx  7860  ltnqex  7863  addnqprlemfl  7873  addnqprlemfu  7874  appdivnq  7877  prmuloclemcalc  7879  prmuloc  7880  mullocprlem  7884  mulnqprlemfl  7889  mulnqprlemfu  7890  ltprordil  7903  ltnqpri  7908  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemdisj  7920  ltexprlemloc  7921  ltexprlemfl  7923  ltexprlemrl  7924  ltexprlemfu  7925  ltexprlemru  7926  ltexpri  7927  lteupri  7931  ltaprlem  7932  recexprlemell  7936  recexprlemelu  7937  recexprlemloc  7945  recexprlempr  7946  recexprlem1ssl  7947  recexprlem1ssu  7948  recexprlemss1u  7950  aptipr  7955  cauappcvgprlemm  7959  cauappcvgprlemlol  7961  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  cauappcvgprlemladdru  7970  cauappcvgprlem1  7973  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprlemm  7982  caucvgprlemlol  7984  caucvgprlemladdfu  7991  caucvgprprlemloccalc  7998  caucvgprprlemnkltj  8003  caucvgprprlemnbj  8007  caucvgprprlemml  8008  caucvgprprlemlol  8012  caucvgprprlemloc  8017  caucvgprprlemexbt  8020  suplocexprlemss  8029  suplocexprlemru  8033  suplocexprlemlub  8038  ltsrprg  8061  caucvgsrlemasr  8104  suplocsrlemb  8120  suplocsrlem  8122  suplocsr  8123  axcaucvglemcau  8212  axpre-suploclemres  8215  negf1o  8654  apreap  8860  apreim  8876  msqge0  8889  mulge0  8892  apti  8895  apsscn  8920  mulap0bad  8932  divadddivap  9000  recnz  9670  lbzbi  9947  xadd4d  10217  ixxss1  10236  ixxss2  10237  ixxss12  10238  iccss2  10276  iccssioo2  10278  iccssico2  10279  iccen  10339  elfzole1  10489  ioom  10619  elicore  10625  flqle  10637  flqltnz  10646  addmodlteq  10759  expclzap  10925  hashennnuni  11140  zfz1isolem1  11208  hashdmprop2dom  11212  swrdsbslen  11354  ccatswrd  11358  ccatpfx  11389  recl  11534  cvg1nlemcau  11665  cvg1nlemres  11666  resqrtth  11712  fimaxre2  11908  climcl  11963  reccn2ap  11994  nnf1o  12058  summodclem3  12062  sumpr  12095  fsump1i  12115  fisumcom2  12120  fsum00  12144  fsumparts  12152  mertenslemi1  12217  prodmodclem3  12257  fprodcom2fi  12308  addsin  12424  subsin  12425  addcos  12428  subcos  12429  sinbnd2  12436  cosbnd2  12437  sin01gt0  12444  cos01gt0  12445  divgcdz  12663  divgcdnn  12667  gcdaddm  12676  bezoutlemstep  12689  dvdsgcdb  12705  dfgcd2  12706  mulgcd  12708  gcdzeq  12714  dvdsmulgcd  12717  sqgcd  12721  bezoutr  12724  lcmval  12756  lcmcllem  12760  gcddvdslcm  12766  lcmgcdlem  12770  lcmgcd  12771  lcmgcdeq  12776  lcmdvdsb  12777  mulgcddvds  12787  rpmulgcd2  12788  qredeu  12790  rpdvds  12792  isprm3  12811  divgcdodd  12836  coprm  12837  rpexp  12846  sqrt2irr  12855  qnumcl  12881  qnumdencoprm  12886  divnumden  12889  numsq  12896  phimullem  12918  eulerthlem1  12920  prmdiveq  12929  prmdivdiv  12930  hashgcdlem  12931  odzcl  12937  reumodprminv  12947  pythagtriplem19  12976  pclemub  12981  pcprendvds  12984  pcprendvds2  12985  pcpre1  12986  pcpremul  12987  pceulem  12988  pceu  12989  pczpre  12991  pczcl  12992  pcgcd1  13022  pc2dvds  13024  pcaddlem  13033  pcmpt  13037  pockthlem  13050  prmunb  13056  4sqlem7  13078  4sqlem8  13079  4sqlem9  13080  4sqlem10  13081  4sqlem14  13098  4sqlem15  13099  4sqlem16  13100  4sqlem17  13101  4sqlem18  13102  ennnfonelemg  13146  ennnfonelemf1  13161  ctiunctlemu1st  13177  nninfdclemf  13192  nninfdclemp1  13193  mgmidcl  13583  gsumfzval  13596  gsumval2  13602  mndlid  13640  prdsmndd  13653  imasmndf1  13659  dfgrp3mlem  13803  grplactf1o  13808  prdsgrpd  13814  prdsinvgd  13815  imasgrpf1  13821  subgsubm  13905  qusgrp  13941  ghmgrp1  13954  ghmf  13956  ghmnsgpreima  13978  kerf1ghm  13983  conjsubg  13986  gsumsplit0  14055  imasrng  14092  srgdilem  14105  srgdi  14110  srglidm  14115  ringdilem  14148  ringdi  14154  ringlidm  14159  imasring  14200  imasringf1  14201  dvdsrcld  14234  unitcld  14245  unitmulcl  14250  unitnegcl  14267  rhmghm  14299  elrhmunit  14314  subrgss  14359  subrgrcl  14363  rrgsupp  14403  lmodvscl  14445  lmodvsdi  14451  lmodvsdir  14452  lsslsp  14569  qusring  14667  crngridl  14670  znunit  14799  znrrg  14800  psrbaglesuppg  14813  psrbagcon  14818  psrbagconcl  14819  psrelbas  14822  psraddcl  14827  mplrcl  14841  uniopn  14858  restbasg  15025  cntop1  15058  cnf  15061  cnpf2  15064  lmtopcnp  15107  psmetdmdm  15181  psmetf  15182  psmet0  15184  xmetf  15207  metf  15208  blhalf  15265  xmetxpbl  15365  ioo2bl  15408  tgioo  15411  cncff  15434  rescncf  15438  cdivcncfap  15461  cnopnap  15468  divcncfap  15471  dedekindeulemeu  15479  dedekindicclemeu  15488  ivthinclemlm  15491  ivthinclemlopn  15493  ivthinclemuopn  15495  ivthinclemdisj  15497  ivthdec  15501  ivthreinc  15502  limcimolemlt  15521  limcimo  15522  limccnpcntop  15532  limccnp2lem  15533  limccnp2cntop  15534  limccoap  15535  eldvap  15539  dvbsssg  15543  dvfgg  15545  dvaddxxbr  15558  dvmulxxbr  15559  dvcoapbr  15564  dvcj  15566  dvfre  15567  dvrecap  15570  plyco  15616  plycj  15618  sin0pilem1  15638  sin0pilem2  15639  pilem3  15640  tanrpcl  15694  tangtx  15695  perfect  15861  lgsne0  15903  lgseisen  15939  lgsquad2lem2  15947  2sqlem8a  15987  2sqlem8  15988  structgrssvtx  16029  edguhgr  16124  umgrpredgv  16134  umgrnloop2  16138  umgr2edg  16194  subuhgr  16259  subumgr  16261  subusgr  16262  wlkpropg  16311  wlkv  16313  wlkvtxeledgg  16331  wlkvtxiedgg  16333  wlk1walkdom  16346  trlsv  16371  clwwlksswrd  16384  clwwlkclwwlkn  16396  eupthv  16433  eupthseg  16439  eupth2lem3lem3fi  16457  eupth2lem3lem4fi  16460  eupth2lemsfi  16465  eulerpathprum  16467  nninfalllem1  16778  iooref1o  16810  gfsumval  16853  alsi1d  16869  alsc1d  16871