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

Theorem simp3d 1095
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 1083 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  simp3bi  1098  f1dom3fv3dif  6565  f1dom3el3dif  6566  oeeui  7727  erinxp  7864  resixp  7985  domssex2  8161  cantnflem1c  8622  cantnflem1  8624  cantnflem3  8626  cantnflem4  8627  fpwwe2lem7  9496  canthnumlem  9508  canthp1lem2  9513  wununi  9566  wunpw  9567  wunpr  9569  lelttrdi  10237  ixxdisj  12228  ixxun  12229  ixxss1  12231  ixxss2  12232  ixxss12  12233  ixxub  12234  ixxlb  12235  lbioo  12244  elicore  12264  iccsupr  12304  icodisj  12335  xov1plusxeqvd  12356  intfracq  12698  fldiv  12699  seqf1olem2  12881  cjmul  13926  icco1  14315  sumtp  14522  rpnnen2lem10  14996  ruclem2  15005  ruclem3  15006  ruclem9  15011  ruclem12  15014  dvdslegcd  15273  crth  15530  eulerthlem1  15533  eulerthlem2  15534  pcpremul  15595  prmreclem2  15668  prmreclem3  15669  4sqlem13  15708  sectcan  16462  sectco  16463  sectmon  16489  monsect  16490  funcid  16577  funcco  16578  funcsect  16579  invfuc  16681  fuciso  16682  coapm  16768  catciso  16804  postr  17000  ipodrsima  17212  psref2  17251  psasym  17257  mhm0  17390  submcl  17400  submmnd  17401  eqger  17691  eqgcpbl  17695  gaorber  17787  orbsta  17792  cayleyth  17881  pmtrrn2  17926  pmtrfinv  17927  pmtrfmvdn0  17928  dfod2  18027  sylow2blem1  18081  sylow2blem3  18083  dprdcntz  18453  dprddisj  18454  dprdffsupp  18459  dpjdisj  18498  ablfac1a  18514  ablfac1b  18515  lmodvsdir  18935  lmhmlin  19083  lbsind  19128  2idlcpbl  19282  assasca  19369  mpfind  19584  mpt2frlmd  20164  mdetunilem2  20467  mdetunilem5  20470  mdetunilem6  20471  mnfnei  21073  cnprcl  21097  lmcvg  21114  lmff  21153  lmcls  21154  lmcnp  21156  fbasssin  21687  flimfil  21820  tgpconncomp  21963  tlmtrg  22040  ustssel  22056  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ustfilxp  22063  tustopn  22122  tususp  22123  imasdsf1olem  22225  xmeter  22285  xmetresbl  22289  tmstopn  22337  metustexhalf  22408  nlmnrg  22530  qdensere  22620  blcvx  22648  tgqioo  22650  icccmplem1  22672  icccmplem2  22673  reconnlem1  22676  cnmpt2pc  22774  iccpnfcnv  22790  phtpcer  22841  phtpcco2  22845  pcohtpy  22866  pcorev2  22874  pcophtb  22875  om1addcl  22879  pi1blem  22885  pi1cpbl  22890  pi1grplem  22895  pi1inv  22898  pi1xfrf  22899  pi1xfr  22901  pi1xfrcnvlem  22902  pi1cof  22905  pi1coghm  22907  cphreccllem  23024  cphsca  23025  cphsubrg  23026  cphsqrtcl2  23032  tchclm  23077  tchcph  23082  lmmcvg  23105  cmetcaulem  23132  lmcau  23157  bcthlem3  23169  bcthlem4  23170  minveclem4c  23242  minveclem2  23243  minveclem3b  23245  minveclem4  23249  minveclem6  23251  ivthicc  23273  ovollb2lem  23302  ovolshftlem1  23323  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem2  23332  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  ioombl1lem1  23372  dyadmaxlem  23411  volivth  23421  vitalilem2  23423  vitalilem4  23425  i1fima2  23491  itg2monolem1  23562  itgcnlem  23601  itgrevallem1  23606  itgreval  23608  itgle  23621  ibladd  23632  iblabslem  23639  itgspliticc  23648  itgsplitioo  23649  ditgcl  23667  ditgswap  23668  ditgsplitlem  23669  limcdif  23685  limcresi  23694  limcres  23695  limccnp  23700  limccnp2  23701  limcun  23704  dvlip  23801  dvlip2  23803  dveq0  23808  dvgt0lem1  23810  dvivthlem1  23816  dvcnvrelem1  23825  dvcnvre  23827  dvfsumlem2  23835  ftc1lem1  23843  ftc1lem2  23844  ftc1a  23845  ftc1lem4  23847  ftc2  23852  ftc2ditglem  23853  itgsubstlem  23856  ply1rem  23968  fta1glem2  23971  ig1pdvds  23981  plyrem  24105  fta1lem  24107  vieta1lem2  24111  aaliou3lem3  24144  pserulm  24221  psercnlem2  24223  psercnlem1  24224  psercn  24225  pserdvlem1  24226  pserdvlem2  24227  abelth2  24241  coseq00topi  24299  coseq0negpitopi  24300  cosordlem  24322  tanord1  24328  efif1olem1  24333  dvloglem  24439  efopnlem1  24447  logreclem  24545  relogbval  24555  nnlogbexp  24564  logbrec  24565  chordthmlem4  24607  quart1  24628  quartlem2  24630  quartlem3  24631  quart  24633  acosbnd  24672  atancj  24682  atanlogsublem  24687  atantan  24695  atanbndlem  24697  atans2  24703  dvatan  24707  atantayl  24709  divsqrtsumlem  24751  ftalem5  24848  basellem5  24856  ppisval  24875  chtleppi  24980  chpchtsum  24989  chpub  24990  mersenne  24997  perfectlem2  25000  dchrinv  25031  rplogsumlem2  25219  chpdifbndlem1  25287  pntibndlem2  25325  pntlema  25330  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemk  25340  pntlemo  25341  pntlemp  25344  pntleml  25345  abvcxp  25349  ostth2lem2  25368  axtgcont1  25412  cgr3simp3  25462  legso  25539  hlln  25547  hltr  25550  btwnhl  25554  mirhl  25619  mirbtwnhl  25620  opphllem4  25687  opphl  25691  hlpasch  25693  cgracgr  25755  cgraswap  25757  cgrahl  25763  cgracol  25764  inagswap  25775  umgrnloopv  26046  umgredgne  26085  usgrnloopvALT  26138  frusgrnn0  26523  cusgrm1rusgr  26534  upgrclwlkcompim  26733  2wlkdlem6  26896  2wlkond  26902  2trlond  26904  numclwwlk2lem1  27356  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2f1oOLD  27366  tncp  27460  grpolidinv  27483  nvs  27646  nvz  27652  nvtri  27653  sspn  27719  minvecolem2  27859  minvecolem4c  27863  minvecolem4  27864  minvecolem5  27865  minvecolem6  27866  adj1  28920  eliccelico  29667  elicoelioo  29668  slmdvsdir  29897  slmd0vs  29905  pmtrto1cl  29977  locfinreflem  30035  cnre2csqlem  30084  sigaclci  30323  unelsiga  30325  insiga  30328  unelldsys  30349  ldsysgenld  30351  sigapildsys  30353  ldgenpisyslem1  30354  measvun  30400  cntmeas  30417  sibfima  30528  signstfveq0  30782  tg5segofs  30879  bnj1018  31158  subfacp1lem3  31290  subfacp1lem4  31291  subfacp1lem5  31292  sconnpht2  31346  sconnpi1  31347  txsconn  31349  resconn  31354  cvmcn  31370  cvmsuni  31377  cvmsdisj  31378  cvmshmeo  31379  cvmlift2lem8  31418  cvmlift2lem13  31423  cvmliftphtlem  31425  cvmliftpht  31426  cvmlift3lem6  31432  msrf  31565  elmsta  31571  mthmpps  31605  mclsppslem  31606  scutun12  32042  slerec  32048  ivthALT  32455  relowlssretop  33341  ibladdnc  33597  iblabsnclem  33603  ftc2nc  33624  dvasin  33626  isbndx  33711  isbnd3  33713  prdsbnd  33722  heiborlem3  33742  iccbnd  33769  rngohomadd  33898  rngohommul  33899  idladdcl  33948  idllmulcl  33949  idlrmulcl  33950  maxidlmax  33972  pridlc  34000  lshpnelb  34589  lshpcmp  34593  oplecon3  34804  opnoncon  34813  hlcvl  34964  dochshpncl  36990  lclkrslem1  37143  lclkrslem2  37144  acongrep  37864  ntrneinex  38692  neicvgmex  38732  gneispace0nelrn  38755  cvgdvgrat  38829  binomcxplemdvbinom  38869  eliocre  40052  iccshift  40062  iccsuble  40063  icoiccdif  40068  mullimc  40166  limccog  40170  limciccioolb  40171  mullimcf  40173  limcperiod  40178  lptioo2  40181  lptioo1  40182  neglimc  40197  addlimc  40198  0ellimcdiv  40199  reclimc  40203  xlimmnfvlem1  40376  xlimpnfvlem1  40380  icccncfext  40418  cncfioobdlem  40427  ditgeqiooicc  40494  iblspltprt  40507  iblcncfioo  40512  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem11  40546  stoweidlem31  40566  stoweidlem36  40571  stoweidlem38  40573  stoweidlem62  40597  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem26  40668  fourierdlem32  40674  fourierdlem33  40675  fourierdlem37  40679  fourierdlem42  40684  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem74  40715  fourierdlem75  40716  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem93  40734  fourierdlem101  40742  fourierdlem107  40748  fourierdlem109  40750  fourierdlem111  40752  salunicl  40854  saluncl  40855  hoidmv1lelem1  41126  hoidmv1lelem3  41128  hoidmvlelem1  41130  ovolval3  41182  iinhoiicclem  41208  smfpreimalt  41261  smfpreimaltf  41266  smfpreimale  41284  issmfgt  41286  smfpreimagt  41291  smfpreimage  41311  sigardiv  41371  sigarcol  41374  sharhght  41375  sigaradd  41376  cevathlem1  41377  cevathlem2  41378  cevath  41379  proththd  41856  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator