MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3d Structured version   Visualization version   GIF version

Theorem simp3d 1167
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1 (𝜑 → (𝜓𝜒𝜃))
Assertion
Ref Expression
simp3d (𝜑𝜃)

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp3 1161 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simp3bi  1170  f1dom3fv3dif  6743  f1dom3el3dif  6744  oeeui  7913  resixp  8174  domssex2  8353  cantnflem1c  8825  cantnflem1  8827  cantnflem3  8829  cantnflem4  8830  fpwwe2lem7  9737  canthnumlem  9749  canthp1lem2  9754  wununi  9807  wunpw  9808  wunpr  9810  lelttrdi  10478  ixxdisj  12402  ixxun  12403  ixxss1  12405  ixxss2  12406  ixxss12  12407  ixxub  12408  ixxlb  12409  lbioo  12418  elicore  12438  iccsupr  12479  icodisj  12512  xov1plusxeqvd  12535  intfracq  12876  fldiv  12877  seqf1olem2  13058  cjmul  14099  icco1  14488  sumtp  14695  rpnnen2lem10  15166  ruclem2  15175  ruclem3  15176  ruclem9  15181  ruclem12  15184  dvdslegcd  15439  crth  15694  eulerthlem1  15697  eulerthlem2  15698  pcpremul  15759  prmreclem2  15832  prmreclem3  15833  4sqlem13  15872  sectcan  16613  sectco  16614  sectmon  16640  monsect  16641  funcid  16728  funcco  16729  funcsect  16730  invfuc  16832  fuciso  16833  coapm  16919  catciso  16955  postr  17152  ipodrsima  17364  psref2  17403  psasym  17409  mhm0  17542  submcl  17552  submmnd  17553  eqger  17840  eqgcpbl  17844  gaorber  17936  orbsta  17941  cayleyth  18030  pmtrrn2  18075  pmtrfinv  18076  pmtrfmvdn0  18077  dfod2  18176  sylow2blem1  18230  sylow2blem3  18232  dprdcntz  18603  dprddisj  18604  dprdffsupp  18609  dpjdisj  18648  ablfac1a  18664  ablfac1b  18665  lmodvsdir  19085  lmhmlin  19236  lbsind  19281  2idlcpbl  19437  assasca  19524  mpfind  19738  mdetunilem2  20624  mdetunilem5  20627  mdetunilem6  20628  mnfnei  21233  cnprcl  21257  lmcvg  21274  lmff  21313  lmcls  21314  lmcnp  21316  fbasssin  21847  flimfil  21980  tgpconncomp  22123  tlmtrg  22200  ustssel  22216  ustincl  22218  ustdiag  22219  ustinvel  22220  ustexhalf  22221  ustfilxp  22223  tustopn  22282  tususp  22283  imasdsf1olem  22385  xmeter  22445  xmetresbl  22449  tmstopn  22497  metustexhalf  22568  nlmnrg  22690  qdensere  22780  blcvx  22808  tgqioo  22810  icccmplem1  22832  icccmplem2  22833  reconnlem1  22836  cnmpt2pc  22934  iccpnfcnv  22950  phtpcer  23001  phtpcco2  23005  pcohtpy  23026  pcorev2  23034  pcophtb  23035  om1addcl  23039  pi1blem  23045  pi1cpbl  23050  pi1grplem  23055  pi1inv  23058  pi1xfrf  23059  pi1xfr  23061  pi1xfrcnvlem  23062  pi1cof  23065  pi1coghm  23067  cphreccllem  23184  cphsca  23185  cphsubrg  23186  cphsqrtcl2  23192  tchclm  23237  tchcph  23242  lmmcvg  23265  cmetcaulem  23292  lmcau  23317  bcthlem3  23329  bcthlem4  23330  minveclem4c  23402  minveclem2  23403  minveclem3b  23405  minveclem4  23409  minveclem6  23411  ivthicc  23433  ovollb2lem  23463  ovolshftlem1  23484  ovolscalem1  23488  ovolicc1  23491  ovolicc2lem2  23493  ovolicc2lem3  23494  ovolicc2lem4  23495  ovolicc2lem5  23496  ioombl1lem1  23533  dyadmaxlem  23572  volivth  23582  vitalilem2  23584  vitalilem4  23586  i1fima2  23654  itg2monolem1  23725  itgcnlem  23764  itgrevallem1  23769  itgreval  23771  itgle  23784  ibladd  23795  iblabslem  23802  itgspliticc  23811  itgsplitioo  23812  ditgcl  23830  ditgswap  23831  ditgsplitlem  23832  limcdif  23848  limcresi  23857  limcres  23858  limccnp  23863  limccnp2  23864  limcun  23867  dvlip  23964  dvlip2  23966  dveq0  23971  dvgt0lem1  23973  dvivthlem1  23979  dvcnvrelem1  23988  dvcnvre  23990  dvfsumlem2  23998  ftc1lem1  24006  ftc1lem2  24007  ftc1a  24008  ftc1lem4  24010  ftc2  24015  ftc2ditglem  24016  itgsubstlem  24019  ply1rem  24131  fta1glem2  24134  ig1pdvds  24144  plyrem  24268  fta1lem  24270  vieta1lem2  24274  aaliou3lem3  24307  pserulm  24384  psercnlem2  24386  psercnlem1  24387  psercn  24388  pserdvlem1  24389  pserdvlem2  24390  abelth2  24404  coseq00topi  24463  coseq0negpitopi  24464  cosordlem  24486  tanord1  24492  efif1olem1  24497  dvloglem  24602  efopnlem1  24610  logreclem  24708  relogbval  24718  nnlogbexp  24727  logbrec  24728  chordthmlem4  24770  quart1  24791  quartlem2  24793  quartlem3  24794  quart  24796  acosbnd  24835  atancj  24845  atanlogsublem  24850  atantan  24858  atanbndlem  24860  atans2  24866  dvatan  24870  atantayl  24872  divsqrtsumlem  24914  ftalem5  25011  basellem5  25019  ppisval  25038  chtleppi  25143  chpchtsum  25152  chpub  25153  mersenne  25160  perfectlem2  25163  dchrinv  25194  rplogsumlem2  25382  chpdifbndlem1  25450  pntibndlem2  25488  pntlema  25493  pntlemb  25494  pntlemg  25495  pntlemh  25496  pntlemr  25499  pntlemj  25500  pntlemf  25502  pntlemk  25503  pntlemo  25504  pntlemp  25507  pntleml  25508  abvcxp  25512  ostth2lem2  25531  axtgcont1  25575  cgr3simp3  25625  legso  25702  hlln  25710  hltr  25713  btwnhl  25717  mirhl  25782  mirbtwnhl  25783  opphllem4  25850  opphl  25854  hlpasch  25856  cgracgr  25918  cgraswap  25920  cgrahl  25926  cgracol  25927  inagswap  25938  umgrnloopv  26209  umgredgne  26249  usgrnloopvALT  26302  frusgrnn0  26689  cusgrm1rusgr  26700  upgrclwlkcompim  26899  2wlkdlem6  27065  2wlkond  27071  2trlond  27073  numclwwlk2lem1  27550  numclwlk2lem2f1o  27553  numclwwlk2lem1OLD  27557  numclwlk2lem2f1oOLD  27560  tncp  27655  grpolidinv  27678  nvs  27840  nvz  27846  nvtri  27847  sspn  27913  minvecolem2  28053  minvecolem4c  28057  minvecolem4  28058  minvecolem5  28059  minvecolem6  28060  adj1  29114  eliccelico  29860  elicoelioo  29861  slmdvsdir  30088  slmd0vs  30096  pmtrto1cl  30168  locfinreflem  30226  cnre2csqlem  30275  sigaclci  30514  unelsiga  30516  insiga  30519  unelldsys  30540  ldsysgenld  30542  sigapildsys  30544  ldgenpisyslem1  30545  measvun  30591  cntmeas  30608  sibfima  30719  signstfveq0  30973  tg5segofs  31070  bnj1018  31349  subfacp1lem3  31481  subfacp1lem4  31482  subfacp1lem5  31483  sconnpht2  31537  sconnpi1  31538  txsconn  31540  resconn  31545  cvmcn  31561  cvmsuni  31568  cvmsdisj  31569  cvmshmeo  31570  cvmlift2lem8  31609  cvmlift2lem13  31614  cvmliftphtlem  31616  cvmliftpht  31617  cvmlift3lem6  31623  msrf  31756  elmsta  31762  mthmpps  31796  mclsppslem  31797  scutun12  32232  slerec  32238  ivthALT  32645  relowlssretop  33521  ibladdnc  33773  iblabsnclem  33779  ftc2nc  33800  dvasin  33802  isbndx  33886  isbnd3  33888  prdsbnd  33897  heiborlem3  33917  iccbnd  33944  rngohomadd  34073  rngohommul  34074  idladdcl  34123  idllmulcl  34124  idlrmulcl  34125  maxidlmax  34147  pridlc  34175  lshpnelb  34758  lshpcmp  34762  oplecon3  34973  opnoncon  34982  hlcvl  35133  dochshpncl  37159  lclkrslem1  37312  lclkrslem2  37313  acongrep  38042  ntrneinex  38869  neicvgmex  38909  gneispace0nelrn  38932  cvgdvgrat  39006  binomcxplemdvbinom  39046  eliocre  40210  iccshift  40219  iccsuble  40220  icoiccdif  40225  mullimc  40322  limccog  40326  limciccioolb  40327  mullimcf  40329  limcperiod  40334  lptioo2  40337  lptioo1  40338  neglimc  40353  addlimc  40354  0ellimcdiv  40355  reclimc  40359  xlimmnfvlem1  40532  xlimpnfvlem1  40536  icccncfext  40574  cncfioobdlem  40583  ditgeqiooicc  40649  iblspltprt  40662  iblcncfioo  40667  itgiccshift  40669  itgperiod  40670  itgsbtaddcnst  40671  stoweidlem11  40701  stoweidlem31  40721  stoweidlem36  40726  stoweidlem38  40728  stoweidlem62  40752  dirkercncflem1  40793  dirkercncflem4  40796  fourierdlem26  40823  fourierdlem32  40829  fourierdlem33  40830  fourierdlem37  40834  fourierdlem42  40839  fourierdlem54  40850  fourierdlem63  40859  fourierdlem64  40860  fourierdlem65  40861  fourierdlem74  40870  fourierdlem75  40871  fourierdlem79  40875  fourierdlem81  40877  fourierdlem82  40878  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  fourierdlem93  40889  fourierdlem101  40897  fourierdlem107  40903  fourierdlem109  40905  fourierdlem111  40907  salunicl  41009  saluncl  41010  hoidmv1lelem1  41281  hoidmv1lelem3  41283  hoidmvlelem1  41285  ovolval3  41337  iinhoiicclem  41363  smfpreimalt  41416  smfpreimaltf  41421  smfpreimale  41439  issmfgt  41441  smfpreimagt  41446  smfpreimage  41466  sigardiv  41526  sigarcol  41529  sharhght  41530  sigaradd  41531  cevathlem1  41532  cevathlem2  41533  cevath  41534  proththd  42100  perfectALTVlem2  42200
  Copyright terms: Public domain W3C validator