Theorem simpld 111

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem is referenced by:  biimp  117  simplbi  272  simprbda  381  simp1  982  eldifad  3113  unssad  3284  opth1  4196  opth  4197  0nelop  4208  epelg  4250  poirr  4267  brrelex1  4624  brrelex  4625  asymref  4970  soirri  4979  sotri  4980  fcnvres  5352  fun11iun  5434  elmpocl1  6016  f1od  6020  f1o2d  6022  oprssdmm  6116  smoiso  6246  tfrlem1  6252  swoer  6505  ecopovtrn  6574  ecopovtrng  6577  elmapssres  6615  pmresg  6618  mapsspm  6624  en1uniel  6746  xpf1o  6786  sbthlemi9  6906  supelti  6942  supsnti  6945  supisoti  6950  ctssdccl  7049  ctfoex  7056  fodjum  7083  en2eleq  7124  djuen  7140  ccfunen  7178  dfplpq2  7268  ltbtwnnqq  7329  enq0tr  7348  elnp1st2nd  7390  prcdnql  7398  prnminu  7403  prloc  7405  genpcdl  7433  addnqprulem  7442  addlocprlemlt  7445  addlocprlemgt  7448  addlocprlem  7449  addlocpr  7450  nqprxx  7460  ltnqex  7463  addnqprlemfl  7473  addnqprlemfu  7474  appdivnq  7477  prmuloclemcalc  7479  prmuloc  7480  mullocprlem  7484  mulnqprlemfl  7489  mulnqprlemfu  7490  ltprordil  7503  ltnqpri  7508  ltexprlemm  7514  ltexprlemopl  7515  ltexprlemlol  7516  ltexprlemopu  7517  ltexprlemupu  7518  ltexprlemdisj  7520  ltexprlemloc  7521  ltexprlemfl  7523  ltexprlemrl  7524  ltexprlemfu  7525  ltexprlemru  7526  ltexpri  7527  lteupri  7531  ltaprlem  7532  recexprlemell  7536  recexprlemelu  7537  recexprlemloc  7545  recexprlempr  7546  recexprlem1ssl  7547  recexprlem1ssu  7548  recexprlemss1u  7550  aptipr  7555  cauappcvgprlemm  7559  cauappcvgprlemlol  7561  cauappcvgprlemladdfu  7568  cauappcvgprlemladdfl  7569  cauappcvgprlemladdru  7570  cauappcvgprlem1  7573  caucvgprlemnkj  7580  caucvgprlemnbj  7581  caucvgprlemm  7582  caucvgprlemlol  7584  caucvgprlemladdfu  7591  caucvgprprlemloccalc  7598  caucvgprprlemnkltj  7603  caucvgprprlemnbj  7607  caucvgprprlemml  7608  caucvgprprlemlol  7612  caucvgprprlemloc  7617  caucvgprprlemexbt  7620  suplocexprlemss  7629  suplocexprlemru  7633  suplocexprlemlub  7638  ltsrprg  7661  caucvgsrlemasr  7704  suplocsrlemb  7720  suplocsrlem  7722  suplocsr  7723  axcaucvglemcau  7812  axpre-suploclemres  7815  negf1o  8251  apreap  8456  apreim  8472  msqge0  8485  mulge0  8488  apti  8491  apsscn  8516  mulap0bad  8527  divadddivap  8594  recnz  9251  lbzbi  9518  xadd4d  9782  ixxss1  9801  ixxss2  9802  ixxss12  9803  iccss2  9841  iccssioo2  9843  iccssico2  9844  iccen  9903  elfzole1  10047  ioom  10153  elicore  10159  flqle  10170  flqltnz  10179  addmodlteq  10290  expclzap  10437  hashennnuni  10646  zfz1isolem1  10704  recl  10746  cvg1nlemcau  10877  cvg1nlemres  10878  resqrtth  10924  fimaxre2  11119  climcl  11172  reccn2ap  11203  nnf1o  11266  summodclem3  11270  sumpr  11303  fsump1i  11323  fisumcom2  11328  fsum00  11352  fsumparts  11360  mertenslemi1  11425  prodmodclem3  11465  fprodcom2fi  11516  addsin  11632  subsin  11633  addcos  11636  subcos  11637  sinbnd2  11644  cosbnd2  11645  sin01gt0  11651  cos01gt0  11652  divgcdz  11846  divgcdnn  11850  gcdaddm  11859  bezoutlemstep  11872  dvdsgcdb  11888  dfgcd2  11889  mulgcd  11891  gcdzeq  11897  dvdsmulgcd  11900  sqgcd  11904  bezoutr  11907  lcmval  11931  lcmcllem  11935  gcddvdslcm  11941  lcmgcdlem  11945  lcmgcd  11946  lcmgcdeq  11951  lcmdvdsb  11952  mulgcddvds  11962  rpmulgcd2  11963  qredeu  11965  rpdvds  11967  isprm3  11986  divgcdodd  12008  coprm  12009  rpexp  12018  sqrt2irr  12027  qnumcl  12053  qnumdencoprm  12058  divnumden  12061  numsq  12068  phimullem  12088  eulerthlem1  12090  prmdiveq  12099  prmdivdiv  12100  hashgcdlem  12101  ennnfonelemg  12115  ennnfonelemf1  12130  ctiunctlemu1st  12146  uniopn  12370  restbasg  12539  cntop1  12572  cnf  12575  cnpf2  12578  lmtopcnp  12621  psmetdmdm  12695  psmetf  12696  psmet0  12698  xmetf  12721  metf  12722  blhalf  12779  xmetxpbl  12879  ioo2bl  12914  tgioo  12917  cncff  12935  rescncf  12939  cdivcncfap  12958  cnopnap  12965  dedekindeulemeu  12971  dedekindicclemeu  12980  ivthinclemlm  12983  ivthinclemlopn  12985  ivthinclemuopn  12987  ivthinclemdisj  12989  ivthdec  12993  limcimolemlt  13004  limcimo  13005  limccnpcntop  13015  limccnp2lem  13016  limccnp2cntop  13017  limccoap  13018  eldvap  13022  dvbsssg  13026  dvfgg  13028  dvaddxxbr  13036  dvmulxxbr  13037  dvcoapbr  13042  dvcj  13044  dvfre  13045  dvrecap  13048  sin0pilem1  13073  sin0pilem2  13074  pilem3  13075  tanrpcl  13129  tangtx  13130  nninfalllem1  13551  iooref1o  13576  alsi1d  13620  alsc1d  13622