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  3340  opth1  4269  opth  4270  0nelop  4281  epelg  4325  poirr  4342  brrelex1  4702  brrelex  4703  asymref  5055  soirri  5064  sotri  5065  fcnvres  5441  fun11iun  5525  elmpocl1  6119  f1od  6126  f1o2d  6128  oprssdmm  6229  smoiso  6360  tfrlem1  6366  swoer  6620  ecopovtrn  6691  ecopovtrng  6694  elmapssres  6732  pmresg  6735  mapsspm  6741  en1uniel  6863  pw2f1odc  6896  xpf1o  6905  sbthlemi9  7031  supelti  7068  supsnti  7071  supisoti  7076  ctssdccl  7177  ctfoex  7184  fodjum  7212  en2eleq  7262  djuen  7278  dftap2  7318  2omotaplemst  7325  exmidapne  7327  ccfunen  7331  dfplpq2  7421  ltbtwnnqq  7482  enq0tr  7501  elnp1st2nd  7543  prcdnql  7551  prnminu  7556  prloc  7558  genpcdl  7586  addnqprulem  7595  addlocprlemlt  7598  addlocprlemgt  7601  addlocprlem  7602  addlocpr  7603  nqprxx  7613  ltnqex  7616  addnqprlemfl  7626  addnqprlemfu  7627  appdivnq  7630  prmuloclemcalc  7632  prmuloc  7633  mullocprlem  7637  mulnqprlemfl  7642  mulnqprlemfu  7643  ltprordil  7656  ltnqpri  7661  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  ltexpri  7680  lteupri  7684  ltaprlem  7685  recexprlemell  7689  recexprlemelu  7690  recexprlemloc  7698  recexprlempr  7699  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1u  7703  aptipr  7708  cauappcvgprlemm  7712  cauappcvgprlemlol  7714  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlem1  7726  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemlol  7737  caucvgprlemladdfu  7744  caucvgprprlemloccalc  7751  caucvgprprlemnkltj  7756  caucvgprprlemnbj  7760  caucvgprprlemml  7761  caucvgprprlemlol  7765  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  suplocexprlemss  7782  suplocexprlemru  7786  suplocexprlemlub  7791  ltsrprg  7814  caucvgsrlemasr  7857  suplocsrlemb  7873  suplocsrlem  7875  suplocsr  7876  axcaucvglemcau  7965  axpre-suploclemres  7968  negf1o  8408  apreap  8614  apreim  8630  msqge0  8643  mulge0  8646  apti  8649  apsscn  8674  mulap0bad  8686  divadddivap  8754  recnz  9419  lbzbi  9690  xadd4d  9960  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccss2  10019  iccssioo2  10021  iccssico2  10022  iccen  10081  elfzole1  10231  ioom  10350  elicore  10356  flqle  10368  flqltnz  10377  addmodlteq  10490  expclzap  10656  hashennnuni  10871  zfz1isolem1  10932  recl  11018  cvg1nlemcau  11149  cvg1nlemres  11150  resqrtth  11196  fimaxre2  11392  climcl  11447  reccn2ap  11478  nnf1o  11541  summodclem3  11545  sumpr  11578  fsump1i  11598  fisumcom2  11603  fsum00  11627  fsumparts  11635  mertenslemi1  11700  prodmodclem3  11740  fprodcom2fi  11791  addsin  11907  subsin  11908  addcos  11911  subcos  11912  sinbnd2  11919  cosbnd2  11920  sin01gt0  11927  cos01gt0  11928  divgcdz  12138  divgcdnn  12142  gcdaddm  12151  bezoutlemstep  12164  dvdsgcdb  12180  dfgcd2  12181  mulgcd  12183  gcdzeq  12189  dvdsmulgcd  12192  sqgcd  12196  bezoutr  12199  lcmval  12231  lcmcllem  12235  gcddvdslcm  12241  lcmgcdlem  12245  lcmgcd  12246  lcmgcdeq  12251  lcmdvdsb  12252  mulgcddvds  12262  rpmulgcd2  12263  qredeu  12265  rpdvds  12267  isprm3  12286  divgcdodd  12311  coprm  12312  rpexp  12321  sqrt2irr  12330  qnumcl  12356  qnumdencoprm  12361  divnumden  12364  numsq  12371  phimullem  12393  eulerthlem1  12395  prmdiveq  12404  prmdivdiv  12405  hashgcdlem  12406  odzcl  12412  reumodprminv  12422  pythagtriplem19  12451  pclemub  12456  pcprendvds  12459  pcprendvds2  12460  pcpre1  12461  pcpremul  12462  pceulem  12463  pceu  12464  pczpre  12466  pczcl  12467  pcgcd1  12497  pc2dvds  12499  pcaddlem  12508  pcmpt  12512  pockthlem  12525  prmunb  12531  4sqlem7  12553  4sqlem8  12554  4sqlem9  12555  4sqlem10  12556  4sqlem14  12573  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  4sqlem18  12577  ennnfonelemg  12620  ennnfonelemf1  12635  ctiunctlemu1st  12651  nninfdclemf  12666  nninfdclemp1  12667  mgmidcl  13021  gsumfzval  13034  gsumval2  13040  mndlid  13076  dfgrp3mlem  13230  grplactf1o  13235  imasgrpf1  13242  subgsubm  13326  qusgrp  13362  ghmgrp1  13375  ghmf  13377  ghmnsgpreima  13399  kerf1ghm  13404  conjsubg  13407  imasrng  13512  srgdilem  13525  srgdi  13530  srglidm  13535  ringdilem  13568  ringdi  13574  ringlidm  13579  imasring  13620  imasringf1  13621  dvdsrcld  13653  unitcld  13664  unitmulcl  13669  unitnegcl  13686  rhmghm  13718  elrhmunit  13733  subrgss  13778  subrgrcl  13782  lmodvscl  13861  lmodvsdi  13867  lmodvsdir  13868  lsslsp  13985  qusring  14083  crngridl  14086  znunit  14215  znrrg  14216  psrbaglesuppg  14226  psrelbas  14228  psraddcl  14232  uniopn  14237  restbasg  14404  cntop1  14437  cnf  14440  cnpf2  14443  lmtopcnp  14486  psmetdmdm  14560  psmetf  14561  psmet0  14563  xmetf  14586  metf  14587  blhalf  14644  xmetxpbl  14744  ioo2bl  14787  tgioo  14790  cncff  14813  rescncf  14817  cdivcncfap  14840  cnopnap  14847  divcncfap  14850  dedekindeulemeu  14858  dedekindicclemeu  14867  ivthinclemlm  14870  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthinclemdisj  14876  ivthdec  14880  ivthreinc  14881  limcimolemlt  14900  limcimo  14901  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  limccoap  14914  eldvap  14918  dvbsssg  14922  dvfgg  14924  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcj  14945  dvfre  14946  dvrecap  14949  plyco  14995  plycj  14997  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  tanrpcl  15073  tangtx  15074  perfect  15237  lgsne0  15279  lgseisen  15315  lgsquad2lem2  15323  2sqlem8a  15363  2sqlem8  15364  nninfalllem1  15652  iooref1o  15678  alsi1d  15725  alsc1d  15727