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  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4374  opth  4375  0nelop  4386  epelg  4433  poirr  4450  brrelex1  4812  brrelex  4813  asymref  5171  soirri  5180  sotri  5181  ffdmd  5557  fcnvres  5573  fun11iun  5658  funopsn  5885  elmpocl1  6279  f1od  6287  f1o2d  6289  oprssdmm  6399  elmpom  6468  fczsupp0  6493  smoiso  6567  tfrlem1  6573  swoer  6829  ecopovtrn  6900  ecopovtrng  6903  elmapssres  6948  pmresg  6951  mapsspm  6957  en1uniel  7085  pw2f1odc  7129  xpf1o  7138  sbthlemi9  7276  fsuppfund  7288  supelti  7336  supsnti  7339  supisoti  7344  ctssdccl  7445  ctfoex  7452  fodjum  7480  en2eleq  7541  djuen  7561  pw1if  7578  dftap2  7611  2omotaplemst  7618  exmidapne  7620  ccfunen  7624  dfplpq2  7715  ltbtwnnqq  7776  enq0tr  7795  elnp1st2nd  7837  prcdnql  7845  prnminu  7850  prloc  7852  genpcdl  7880  addnqprulem  7889  addlocprlemlt  7892  addlocprlemgt  7895  addlocprlem  7896  addlocpr  7897  nqprxx  7907  ltnqex  7910  addnqprlemfl  7920  addnqprlemfu  7921  appdivnq  7924  prmuloclemcalc  7926  prmuloc  7927  mullocprlem  7931  mulnqprlemfl  7936  mulnqprlemfu  7937  ltprordil  7950  ltnqpri  7955  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemdisj  7967  ltexprlemloc  7968  ltexprlemfl  7970  ltexprlemrl  7971  ltexprlemfu  7972  ltexprlemru  7973  ltexpri  7974  lteupri  7978  ltaprlem  7979  recexprlemell  7983  recexprlemelu  7984  recexprlemloc  7992  recexprlempr  7993  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1u  7997  aptipr  8002  cauappcvgprlemm  8006  cauappcvgprlemlol  8008  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlemladdru  8017  cauappcvgprlem1  8020  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemm  8029  caucvgprlemlol  8031  caucvgprlemladdfu  8038  caucvgprprlemloccalc  8045  caucvgprprlemnkltj  8050  caucvgprprlemnbj  8054  caucvgprprlemml  8055  caucvgprprlemlol  8059  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  suplocexprlemss  8076  suplocexprlemru  8080  suplocexprlemlub  8085  ltsrprg  8108  caucvgsrlemasr  8151  suplocsrlemb  8167  suplocsrlem  8169  suplocsr  8170  axcaucvglemcau  8259  axpre-suploclemres  8262  negf1o  8703  apreap  8909  apreim  8925  msqge0  8938  mulge0  8941  apti  8944  apsscn  8969  mulap0bad  8981  divadddivap  9051  recnz  9722  lbzbi  9999  xadd4d  10270  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccss2  10329  iccssioo2  10331  iccssico2  10332  iccen  10392  elfzole1  10546  infssfzcldc  10652  infssfzledc  10653  ioom  10678  elicore  10684  flqle  10696  flqltnz  10705  addmodlteq  10818  expclzap  10984  hashennnuni  11201  zfz1isolem1  11275  hashdmprop2dom  11279  swrdsbslen  11421  ccatswrd  11425  ccatpfx  11456  recl  11601  sq01  11643  cvg1nlemcau  11733  cvg1nlemres  11734  resqrtth  11780  fimaxre2  11976  climcl  12031  reccn2ap  12062  nnf1o  12126  summodclem3  12130  sumpr  12163  fsump1i  12183  fisumcom2  12188  fsum00  12212  fsumparts  12220  mertenslemi1  12285  prodmodclem3  12325  fprodcom2fi  12376  addsin  12492  subsin  12493  addcos  12496  subcos  12497  sinbnd2  12504  cosbnd2  12505  sin01gt0  12512  cos01gt0  12513  divgcdz  12731  divgcdnn  12735  gcdaddm  12744  bezoutlemstep  12757  dvdsgcdb  12773  dfgcd2  12774  mulgcd  12776  gcdzeq  12782  dvdsmulgcd  12785  sqgcd  12789  bezoutr  12792  lcmval  12824  lcmcllem  12828  gcddvdslcm  12834  lcmgcdlem  12838  lcmgcd  12839  lcmgcdeq  12844  lcmdvdsb  12845  mulgcddvds  12855  rpmulgcd2  12856  qredeu  12858  rpdvds  12860  isprm3  12879  divgcdodd  12904  coprm  12905  rpexp  12914  sqrt2irr  12923  qnumcl  12949  qnumdencoprm  12954  divnumden  12957  numsq  12964  phimullem  12986  eulerthlem1  12988  prmdiveq  12997  prmdivdiv  12998  hashgcdlem  12999  odzcl  13005  reumodprminv  13015  pythagtriplem19  13044  pclemub  13049  pcprendvds  13052  pcprendvds2  13053  pcpre1  13054  pcpremul  13055  pceulem  13056  pceu  13057  pczpre  13059  pczcl  13060  pcgcd1  13090  pc2dvds  13092  pcaddlem  13101  pcmpt  13105  pockthlem  13118  prmunb  13124  4sqlem7  13146  4sqlem8  13147  4sqlem9  13148  4sqlem10  13149  4sqlem14  13166  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  4sqlem18  13170  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilem4  13224  ballotfilemi1  13228  ballotfilemimin  13232  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemsv  13236  ballotfilemsgt1  13237  ballotfilemsdom  13238  ballotfilemsel1i  13239  ballotfilemsf1o  13240  ballotfilemsi  13241  ballotfilemsima  13242  ballotfilemscr  13245  ballotfilemrv  13246  ballotfilemrv2  13248  ballotfilemro  13249  ballotfilemfrc  13253  ballotfilemfrci  13254  ballotfilemfrceq  13255  ballotfilemfrcn0  13256  ballotfilemrc  13257  ballotfilemirc  13258  ballotfilemrinv0  13259  ballotfilem1ri  13261  ennnfonelemg  13277  ennnfonelemf1  13292  ctiunctlemu1st  13308  nninfdclemf  13323  nninfdclemp1  13324  mgmidcl  13681  gzsumfzval  13694  gzsumval2  13697  mndlid  13731  imasmndf1  13744  dfgrp3mlem  13886  grplactf1o  13891  imasgrpf1  13898  subgsubm  13982  qusgrp  14018  ghmgrp1  14031  ghmf  14033  ghmnsgpreima  14055  kerf1ghm  14060  conjsubg  14063  gzsumsplit0  14131  gsumvalfi  14135  prdsmndd  14177  prdsgrpd  14180  prdsinvgd  14181  imasrng  14238  srgdilem  14256  srgdi  14261  srglidm  14266  ringdilem  14299  ringdi  14306  ringlidm  14311  imasring  14352  imasringf1  14353  dvdsrcld  14387  unitcld  14398  unitmulcl  14403  unitnegcl  14420  rhmghm  14452  elrhmunit  14467  subrgss  14513  subrgrcl  14517  rrgsupp  14557  lmodvscl  14624  lmodvsdi  14631  lmodvsdir  14632  lsslsp  14749  qusring  14847  crngridl  14850  znunit  14977  znrrg  14978  assaass  14987  assalmod  14989  psrbaglesuppg  15040  psrbagcon  15045  psrbagconcl  15046  psrelbas  15049  psraddcl  15054  mplrcl  15068  uniopn  15085  restbasg  15252  cntop1  15285  cnf  15288  cnpf2  15291  lmtopcnp  15334  psmetdmdm  15408  psmetf  15409  psmet0  15411  xmetf  15434  metf  15435  blhalf  15492  xmetxpbl  15592  ioo2bl  15635  tgioo  15638  cncff  15661  rescncf  15665  cdivcncfap  15688  cnopnap  15695  divcncfap  15698  dedekindeulemeu  15706  dedekindicclemeu  15715  ivthinclemlm  15718  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthinclemdisj  15724  ivthdec  15728  ivthreinc  15729  limcimolemlt  15748  limcimo  15749  limccnpcntop  15759  limccnp2lem  15760  limccnp2cntop  15761  limccoap  15762  eldvap  15766  dvbsssg  15770  dvfgg  15772  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcj  15793  dvfre  15794  dvrecap  15797  plyco  15843  plycj  15845  sin0pilem1  15865  sin0pilem2  15866  pilem3  15867  tanrpcl  15921  tangtx  15922  perfect  16098  lgsne0  16140  lgseisen  16176  lgsquad2lem2  16184  2sqlem8a  16224  2sqlem8  16225  structgrssvtx  16266  edguhgr  16361  umgrpredgv  16371  umgrnloop2  16375  umgr2edg  16431  subuhgr  16496  subumgr  16498  subusgr  16499  wlkpropg  16548  wlkv  16550  wlkvtxeledgg  16568  wlkvtxiedgg  16570  wlk1walkdom  16583  trlsv  16608  clwwlksswrd  16621  clwwlkclwwlkn  16633  eupthv  16670  eupthseg  16676  eupth2lem3lem3fi  16694  eupth2lem3lem4fi  16697  eupth2lemsfi  16702  eulerpathprum  16704  nninfalllem1  17025  iooref1o  17057  als1d  17107  rals1d  17109  alseu1d  17143  ralseu1d  17145