Theorem simp1d 1148

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 1142	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp1bi  1151  f1dom3fv3dif  7219  f1dom3el3dif  7220  f1prex  7235  oeeui  8535  oeeu  8536  domssex2  9072  domssex  9073  cantnflem1a  9604  cantnflem1b  9605  cantnflem1c  9606  cantnflem1d  9607  cantnflem1  9608  cantnflem3  9610  cantnflem4  9611  fpwwe2lem6  10557  canthnumlem  10569  canthp1lem2  10574  wuntr  10626  lelttrdi  11306  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  ixxdisj  13311  ixxun  13312  ixxss1  13314  ixxss2  13315  ixxss12  13316  ixxub  13317  ixxlb  13318  iccss2  13368  iocssre  13378  icossre  13379  iccssre  13380  icodisj  13427  iccf1o  13447  xov1plusxeqvd  13449  fzen  13493  intfracq  13816  fldiv  13817  remul  15089  01sqrexlem6  15207  resqrtth  15215  sqrtth  15325  ruclem6  16200  ruclem9  16203  ruclem12  16206  gcdn0cl  16469  crth  16746  phimullem  16747  eulerthlem1  16749  eulerthlem2  16750  pcpremul  16812  prmreclem3  16887  sectcan  17720  sectco  17721  sectmon  17747  monsect  17748  funcf1  17831  funcsect  17837  invfuc  17942  coapm  18036  catciso  18076  psrel  18533  pstr  18541  mhmf  18755  submss  18775  eqger  19151  eqgcpbl  19155  gaorber  19281  orbstafun  19284  cayleyth  19388  dprdgrp  19980  dprdff  19987  ablfac1a  20044  ablfac1b  20045  lmodvscl  20875  lbsss  21074  2idlcpblrng  21271  evlsval3  22072  mpfind  22098  mdetunilem2  22603  mdetunilem5  22606  mdetunilem6  22607  chfacfisfcpmat  22845  cnptop1  23232  lmfpm  23285  lmff  23291  lmcnp  23294  flimtop  23955  tlmtmd  24177  ustssxp  24195  ustdiag  24199  ustfilxp  24203  ustbas2  24215  tusbas  24257  imasdsf1olem  24363  xmeter  24423  tmsbas  24473  metustexhalf  24546  nlmngp  24667  qdensere  24759  blcvx  24788  tgqioo  24790  icccmplem2  24814  reconnlem1  24817  cnmpopc  24920  icoopnst  24931  iocopnst  24932  iccpnfcnv  24936  phtpcer  24987  phtpcco2  24991  pcohtpylem  25011  pcohtpy  25012  pcopt  25014  pcopt2  25015  pcorevlem  25018  pcorev2  25020  pcophtb  25021  om1addcl  25025  pi1grplem  25041  pi1inv  25044  pi1xfrf  25045  pi1xfr  25047  pi1xfrcnvlem  25048  pi1xfrcnv  25049  pi1cof  25051  pi1coghm  25053  cphphl  25163  cphreccllem  25170  cphsqrtcl2  25178  phclm  25224  tcphcph  25229  lmcau  25305  bcthlem4  25319  minveclem4c  25417  minveclem2  25418  minveclem3b  25420  minveclem4  25424  minveclem6  25426  ivthicc  25450  ovolfsval  25462  ovollb2lem  25480  ovolshftlem1  25501  ovolscalem1  25505  ovolicc2lem2  25510  ovolicc2lem5  25513  ovolicopnf  25516  ioombl1lem1  25550  ioombl1lem3  25552  ioombl1lem4  25553  uniioovol  25571  uniioombllem2a  25574  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem6  25580  vitalilem2  25601  vitalilem3  25602  vitalilem4  25603  i1ff  25668  itg2monolem1  25742  itgreval  25789  ibladd  25813  iblabslem  25820  itgspliticc  25829  itgsplitioo  25830  ditgcl  25850  ditgswap  25851  ditgsplitlem  25852  ditgsplit  25853  limcresi  25877  dvlip2  25987  dveq0  25992  dvcnvre  26011  dvfsumlem2  26019  ftc1a  26029  ply1rem  26156  facth1  26157  fta1glem1  26158  fta1glem2  26159  ig1pcl  26169  ig1pdvds  26170  plyrem  26296  facth  26297  vieta1lem1  26301  vieta1lem2  26302  aaliou3lem3  26335  aaliou3lem7  26340  pserulm  26412  psercnlem2  26414  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  pserdv  26419  abelth2  26432  coseq00topi  26491  coseq0negpitopi  26492  cosordlem  26519  efif1olem1  26531  dvloglem  26637  loglesqrt  26750  relogbval  26761  nnlogbexp  26770  logbrec  26771  quart1  26845  quartlem2  26847  quartlem3  26848  quartlem4  26849  quart  26850  asinsinlem  26880  atanlogsublem  26904  atans2  26920  dvatan  26924  rlimcnp2  26955  divsqrtsumlem  26968  ftalem5  27065  ftalem7  27067  basellem4  27072  basellem5  27073  perfectlem2  27218  dchrinv  27249  chpdifbndlem1  27541  pntibndlem2  27579  pntlema  27584  pntlemb  27585  pntlemg  27586  pntlemh  27587  pntlemn  27588  pntlemq  27589  pntlemr  27590  pntlemj  27591  pntlemf  27593  pntlemk  27594  pntlemo  27595  pntlemp  27598  pntleml  27599  abvcxp  27603  cutscl  27799  cutsun12  27807  ltsrec  27818  addsproplem6  27991  addsprop  27993  addscld  27997  negsproplem6  28050  negsprop  28052  mulsproplem11  28143  mulsproplem12  28144  axtgbtwnid  28559  cgr3simp1  28613  hlne1  28698  hltr  28703  btwnhl  28707  mirhl  28772  opphllem4  28843  hlpasch  28849  inagswap  28934  inagne1  28935  dfcgrg2  28956  wlkf  29708  wlk1ewlk  29733  2wlkdlem6  30024  2wlkond  30030  2trlond  30032  grpofo  30595  vcablo  30665  nvvc  30711  sspba  30823  sspg  30824  minvecolem2  30971  minvecolem4c  30975  minvecolem4  30976  minvecolem5  30977  minvecolem6  30978  eleigveccl  32055  tpssad  32634  xrofsup  32866  eliccelico  32876  elicoelioo  32877  cyc3evpm  33238  slmdvscl  33302  slmdvsass  33305  imaslmod  33443  prmidlidl  33534  mxidlidl  33553  0ringmon1p  33647  irngss  33878  algextdeglem1  33908  constrsqrtcl  33970  baselsiga  34306  insiga  34328  ldsysgenld  34351  sigapildsys  34353  ldgenpisyslem1  34354  measfrge0  34394  sibfmbl  34526  eulerpartlemt  34562  eulerpartlemmf  34566  probfinmeasbALTV  34620  tg5segofs  34864  pfxwlk  35359  revwlk  35360  subgrwlk  35367  subfacp1lem2a  35415  subfacp1lem2b  35416  subfacp1lem3  35417  subfacp1lem4  35418  subfacp1lem5  35419  sconnpht2  35473  sconnpi1  35474  cvxsconn  35478  cvmlift2lem3  35540  cvmlift2lem5  35542  cvmlift2lem6  35543  cvmlift2lem7  35544  cvmlift2lem12  35549  cvmliftphtlem  35552  cvmliftpht  35553  cvmlift3lem2  35555  cvmlift3lem4  35557  cvmlift3lem5  35558  cvmlift3lem6  35559  msrf  35777  elmsta  35783  mthmpps  35817  mclsppslem  35818  mclspps  35819  weiunfrlem  36699  weiunpo  36700  weiunso  36701  weiunfr  36702  weiunse  36703  iblabsnclem  38057  dvasin  38078  isbnd3  38158  heiborlem3  38187  iccbnd  38214  rngohomf  38340  idlss  38390  lshplss  39480  opoccl  39693  opococ  39694  oplecon3  39698  hloml  39856  lclkrslem1  42036  lclkrslem2  42037  dvrelog2  42556  dvrelog3  42557  aks4d1p1p5  42567  primrootsunit1  42589  primrootscoprmpow  42591  primrootscoprbij  42594  primrootspoweq0  42598  aks6d1c1p2  42601  aks6d1c1p3  42602  aks6d1c1p4  42603  aks6d1c1p5  42604  aks6d1c1p7  42605  aks6d1c1p6  42606  aks6d1c1p8  42607  aks6d1c2lem3  42618  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c6lem4  42665  aks6d1c6isolem1  42666  aks6d1c6isolem2  42667  aks6d1c6lem5  42669  aks5lem1  42678  aks5lem2  42679  aks5lem3a  42681  flt4lem5f  43114  flt4lem7  43116  nna4b4nsq  43117  eliccre  45957  eliocre  45961  icoiccdif  45976  limccog  46072  lptioo1  46084  cncfiooicclem1  46343  ditgeqiooicc  46410  stoweidlem30  46480  stoweidlem31  46481  stoweidlem38  46488  stoweidlem44  46494  fourierdlem26  46583  fourierdlem32  46589  fourierdlem33  46590  fourierdlem37  46594  fourierdlem42  46599  fourierdlem54  46610  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem69  46625  fourierdlem79  46635  fourierdlem82  46638  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem111  46667  0sal  46770  hoidmv1lelem3  47043  smfdmss  47183  sigardiv  47311  sigarcol  47314  sharhght  47315  sigaradd  47316  cevathlem1  47317  cevathlem2  47318  cevath  47319  nthrucw  47338  proththd  48099  perfectALTVlem2  48220  isuspgrim0  48392  gpgnbgrvtx0  48572  gpgnbgrvtx1  48573  itsclc0yqsol  49262  imaf1hom  49605