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

Theorem simp3d 1141
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 1135 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp3bi  1144  f1dom3fv3dif  7018  f1dom3el3dif  7019  oeeui  8224  resixp  8493  domssex2  8674  cantnflem1c  9147  cantnflem1  9149  cantnflem3  9151  cantnflem4  9152  fpwwe2lem7  10056  canthnumlem  10068  canthp1lem2  10073  wununi  10126  wunpw  10127  wunpr  10129  lelttrdi  10800  ixxdisj  12750  ixxun  12751  ixxss1  12753  ixxss2  12754  ixxss12  12755  ixxub  12756  ixxlb  12757  lbioo  12766  elicore  12786  iccsupr  12829  icodisj  12863  xov1plusxeqvd  12885  intfracq  13231  fldiv  13232  seqf1olem2  13415  cjmul  14501  icco1  14897  sumtp  15104  rpnnen2lem10  15576  ruclem2  15585  ruclem3  15586  ruclem9  15591  ruclem12  15594  dvdslegcd  15851  crth  16113  eulerthlem1  16116  eulerthlem2  16117  pcpremul  16178  prmreclem2  16251  prmreclem3  16252  4sqlem13  16291  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcid  17140  funcco  17141  funcsect  17142  invfuc  17244  fuciso  17245  coapm  17331  catciso  17367  postr  17563  ipodrsima  17775  psref2  17814  psasym  17820  mhm0  17964  submcl  17977  submmnd  17978  eqger  18330  eqgcpbl  18334  gaorber  18438  orbsta  18443  cayleyth  18543  pmtrrn2  18588  pmtrfinv  18589  pmtrfmvdn0  18590  dfod2  18691  sylow2blem1  18745  sylow2blem3  18747  dprdcntz  19130  dprddisj  19131  dprdffsupp  19136  dpjdisj  19175  ablfac1a  19191  ablfac1b  19192  lmodvsdir  19658  lmhmlin  19807  lbsind  19852  2idlcpbl  20007  assasca  20558  mpfind  20786  mdetunilem2  21225  mdetunilem5  21228  mdetunilem6  21229  mnfnei  21833  cnprcl  21857  lmcvg  21874  lmff  21913  lmcls  21914  lmcnp  21916  fbasssin  22448  flimfil  22581  tgpconncomp  22725  tlmtrg  22802  ustssel  22818  ustincl  22820  ustdiag  22821  ustinvel  22822  ustexhalf  22823  ustfilxp  22825  tustopn  22884  tususp  22885  imasdsf1olem  22987  xmeter  23047  xmetresbl  23051  tmstopn  23099  metustexhalf  23170  nlmnrg  23292  qdensere  23382  blcvx  23410  tgqioo  23412  icccmplem1  23434  icccmplem2  23435  reconnlem1  23438  cnmpopc  23540  iccpnfcnv  23556  phtpcer  23607  phtpcco2  23611  pcohtpy  23632  pcorev2  23640  pcophtb  23641  om1addcl  23645  pi1blem  23651  pi1cpbl  23656  pi1grplem  23661  pi1inv  23664  pi1xfrf  23665  pi1xfr  23667  pi1xfrcnvlem  23668  pi1cof  23671  pi1coghm  23673  cphreccllem  23790  cphsca  23791  cphsubrg  23792  cphsqrtcl2  23798  phclm  23843  tcphcph  23848  lmmcvg  23872  cmetcaulem  23899  lmcau  23924  bcthlem3  23937  bcthlem4  23938  minveclem4c  24036  minveclem2  24037  minveclem3b  24039  minveclem4  24043  minveclem6  24045  ivthicc  24069  ovollb2lem  24099  ovolshftlem1  24120  ovolscalem1  24124  ovolicc1  24127  ovolicc2lem2  24129  ovolicc2lem3  24130  ovolicc2lem4  24131  ovolicc2lem5  24132  ioombl1lem1  24169  dyadmaxlem  24208  volivth  24218  vitalilem2  24220  vitalilem4  24222  i1fima2  24290  itg2monolem1  24361  itgcnlem  24400  itgrevallem1  24405  itgreval  24407  itgle  24420  ibladd  24431  iblabslem  24438  itgspliticc  24447  itgsplitioo  24448  ditgcl  24468  ditgswap  24469  ditgsplitlem  24470  limcdif  24486  limcresi  24495  limcres  24496  limccnp  24501  limccnp2  24502  limcun  24505  dvlip  24603  dvlip2  24605  dveq0  24610  dvgt0lem1  24612  dvivthlem1  24618  dvcnvrelem1  24627  dvcnvre  24629  dvfsumlem2  24637  ftc1lem1  24645  ftc1lem2  24646  ftc1a  24647  ftc1lem4  24649  ftc2  24654  ftc2ditglem  24655  itgsubstlem  24658  ply1rem  24771  fta1glem2  24774  ig1pdvds  24784  plyrem  24908  fta1lem  24910  vieta1lem2  24914  aaliou3lem3  24947  pserulm  25024  psercnlem2  25026  psercnlem1  25027  psercn  25028  pserdvlem1  25029  pserdvlem2  25030  abelth2  25044  coseq00topi  25102  coseq0negpitopi  25103  cosordlem  25129  tanord1  25136  efif1olem1  25141  dvloglem  25246  efopnlem1  25254  logreclem  25355  relogbval  25365  nnlogbexp  25374  logbrec  25375  chordthmlem4  25428  quart1  25449  quartlem2  25451  quartlem3  25452  quart  25454  acosbnd  25493  atancj  25503  atanlogsublem  25508  atantan  25516  atanbndlem  25518  atans2  25524  dvatan  25528  atantayl  25530  divsqrtsumlem  25572  ftalem5  25669  basellem5  25677  ppisval  25696  chtleppi  25801  chpchtsum  25810  chpub  25811  mersenne  25818  perfectlem2  25821  dchrinv  25852  rplogsumlem2  26076  chpdifbndlem1  26144  pntibndlem2  26182  pntlema  26187  pntlemb  26188  pntlemg  26189  pntlemh  26190  pntlemr  26193  pntlemj  26194  pntlemf  26196  pntlemk  26197  pntlemo  26198  pntlemp  26201  pntleml  26202  abvcxp  26206  ostth2lem2  26225  axtgcont1  26269  cgr3simp3  26323  legso  26400  hlln  26408  hltr  26411  btwnhl  26415  mirhl  26480  mirbtwnhl  26481  opphllem4  26551  opphl  26555  hlpasch  26557  cgracgr  26619  cgraswap  26621  cgrahl  26628  cgracol  26629  inagswap  26642  inagne3  26645  dfcgrg2  26664  umgrnloopv  26906  umgredgne  26945  usgrnloopvALT  26998  frusgrnn0  27368  cusgrm1rusgr  27379  upgrclwlkcompim  27577  2wlkdlem6  27724  2wlkond  27730  2trlond  27732  numclwwlk2lem1  28168  numclwlk2lem2f1o  28171  tncp  28268  grpolidinv  28291  nvs  28453  nvz  28459  nvtri  28460  sspn  28526  minvecolem2  28665  minvecolem4c  28669  minvecolem4  28670  minvecolem5  28671  minvecolem6  28672  adj1  29723  eliccelico  30515  elicoelioo  30516  prmdvdsbc  30547  pmtrto1cl  30777  cyc3evpm  30828  slmdvsdir  30880  slmd0vs  30888  prmidl  31000  prmidlc  31009  qsidomlem2  31011  mxidlmax  31019  locfinreflem  31168  cnre2csqlem  31214  sigaclci  31452  unelsiga  31454  insiga  31457  unelldsys  31478  ldsysgenld  31480  sigapildsys  31482  ldgenpisyslem1  31483  measvun  31529  cntmeas  31546  sibfima  31657  signstfveq0  31908  tg5segofs  32005  bnj1018g  32296  bnj1018  32297  pfxwlk  32431  revwlk  32432  spthcycl  32437  acycgrcycl  32455  subfacp1lem3  32490  subfacp1lem4  32491  subfacp1lem5  32492  sconnpht2  32546  sconnpi1  32547  txsconn  32549  resconn  32554  cvmcn  32570  cvmsuni  32577  cvmsdisj  32578  cvmshmeo  32579  cvmlift2lem8  32618  cvmlift2lem13  32623  cvmliftphtlem  32625  cvmliftpht  32626  cvmlift3lem6  32632  msrf  32850  elmsta  32856  mthmpps  32890  mclsppslem  32891  scutun12  33332  slerec  33338  ivthALT  33744  relowlssretop  34729  ibladdnc  35063  iblabsnclem  35069  ftc2nc  35088  dvasin  35090  isbndx  35169  isbnd3  35171  prdsbnd  35180  heiborlem3  35200  iccbnd  35227  rngohomadd  35356  rngohommul  35357  idladdcl  35406  idllmulcl  35407  idlrmulcl  35408  maxidlmax  35430  pridlc  35458  eqvreltr  35951  lshpnelb  36229  lshpcmp  36233  oplecon3  36444  opnoncon  36453  hlcvl  36604  dochshpncl  38629  lclkrslem1  38782  lclkrslem2  38783  fzne2d  39217  metakunt8  39307  metakunt20  39319  metakunt21  39320  metakunt22  39321  metakunt24  39323  metakunt25  39324  acongrep  39842  ntrneinex  40704  neicvgmex  40744  gneispace0nelrn  40767  cvgdvgrat  40942  binomcxplemdvbinom  40982  eliocre  42077  iccshift  42086  iccsuble  42087  icoiccdif  42092  mullimc  42189  limccog  42193  limciccioolb  42194  mullimcf  42196  limcperiod  42201  lptioo2  42204  lptioo1  42205  neglimc  42220  addlimc  42221  0ellimcdiv  42222  reclimc  42226  xlimmnfvlem1  42405  xlimpnfvlem1  42409  icccncfext  42460  cncfioobdlem  42469  ditgeqiooicc  42533  iblspltprt  42546  iblcncfioo  42551  itgiccshift  42553  itgperiod  42554  itgsbtaddcnst  42555  stoweidlem11  42584  stoweidlem31  42604  stoweidlem36  42609  stoweidlem38  42611  stoweidlem62  42635  dirkercncflem1  42676  dirkercncflem4  42679  fourierdlem26  42706  fourierdlem32  42712  fourierdlem33  42713  fourierdlem37  42717  fourierdlem42  42722  fourierdlem54  42733  fourierdlem63  42742  fourierdlem64  42743  fourierdlem65  42744  fourierdlem74  42753  fourierdlem75  42754  fourierdlem79  42758  fourierdlem81  42760  fourierdlem82  42761  fourierdlem89  42768  fourierdlem90  42769  fourierdlem91  42770  fourierdlem93  42772  fourierdlem101  42780  fourierdlem107  42786  fourierdlem109  42788  fourierdlem111  42790  salunicl  42889  saluncl  42890  hoidmv1lelem1  43161  hoidmv1lelem3  43163  hoidmvlelem1  43165  ovolval3  43217  iinhoiicclem  43243  smfpreimalt  43296  smfpreimaltf  43301  smfpreimale  43319  issmfgt  43321  smfpreimagt  43326  smfpreimage  43346  sigardiv  43406  sigarcol  43409  sharhght  43410  sigaradd  43411  cevathlem1  43412  cevathlem2  43413  cevath  43414  proththd  44063  perfectALTVlem2  44171
  Copyright terms: Public domain W3C validator