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

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

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp2 1082 . 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:  simp2bi  1097  f1dom3fv3dif  6565  f1dom3el3dif  6566  f1prex  6579  oeeui  7727  erinxp  7864  resixp  7985  domssex  8162  cantnflem1a  8620  cantnflem1d  8623  cantnflem3  8626  cantnflem4  8627  fpwwe2lem7  9496  canthnumlem  9508  canthp1lem2  9513  wun0  9578  lelttrdi  10237  supmullem2  11032  supmul  11033  ixxdisj  12228  ixxun  12229  ixxss1  12231  ixxss2  12232  ixxss12  12233  ixxub  12234  ixxlb  12235  ubioo  12245  elicore  12264  iccgelb  12268  iccss2  12282  icodisj  12335  xov1plusxeqvd  12356  fldiv  12699  immul  13920  sqrtge0  14042  sqrtrege0  14149  icco1  14315  ruclem2  15005  ruclem3  15006  ruclem8  15010  ruclem12  15014  gcddvds  15272  crth  15530  phimullem  15531  eulerthlem1  15533  eulerthlem2  15534  prmreclem3  15669  sectcan  16462  sectco  16463  sectmon  16489  monsect  16490  funcixp  16574  funcsect  16579  invfuc  16681  coapm  16768  catciso  16804  posasymb  16999  ipodrsima  17212  pstr2  17252  psdmrn  17254  psref  17255  mhmlin  17389  subm0cl  17399  eqger  17691  eqgcpbl  17695  gaorber  17787  orbstafun  17790  cayleyth  17881  pmtrrn2  17926  pmtrfinv  17927  dfod2  18027  sylow2blem1  18081  dprdf  18451  dprdff  18457  dprdfcl  18458  dprdsplit  18493  dpjcntz  18497  ablfac1a  18514  ablfac1b  18515  lmodvsdi  18934  lbssp  19127  2idlcpbl  19282  assaring  19368  mpff  19581  mpfaddcl  19582  mpfmulcl  19583  mpfind  19584  pf1rcl  19761  mpfpf1  19763  mdetunilem2  20467  mdetunilem5  20470  mdetunilem6  20471  chfacfisfcpmat  20708  pnfnei  21072  cnptop2  21095  lmcl  21149  lmcnp  21156  flimfil  21820  tlmlmod  22039  ustbasel  22057  ustincl  22058  ustinvel  22060  ustfilxp  22063  tusunif  22120  imasdsf1olem  22225  xmeter  22285  tmsds  22336  metustexhalf  22408  nlmlmod  22529  qdensere  22620  blcvx  22648  tgqioo  22650  icccmplem2  22673  reconnlem1  22676  cnmpt2pc  22774  phtpcer  22841  phtpcco2  22845  pcohtpylem  22865  pcohtpy  22866  pcophtb  22875  om1addcl  22879  pi1blem  22885  pi1cpbl  22890  pi1grplem  22895  pi1inv  22898  pi1xfrf  22899  pi1xfr  22901  pi1xfrcnvlem  22902  pi1cof  22905  pi1coghm  22907  cphnlm  23018  cphsqrtcl2  23032  tchcph  23082  lmcau  23157  bcthlem4  23170  minveclem4c  23242  minveclem2  23243  minveclem3b  23245  minveclem4  23249  minveclem6  23251  ivthicc  23273  ovolfsval  23285  ovollb2lem  23302  ovolshftlem1  23323  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem2  23332  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicopnf  23338  ioombl1lem1  23372  ioombl1lem3  23374  ioombl1lem4  23375  uniioovol  23393  uniioombllem2a  23396  uniioombllem2  23397  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  uniioombllem6  23402  dyadmaxlem  23411  volivth  23421  vitalilem2  23423  vitalilem5  23426  i1frn  23489  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  limccnp  23700  limccnp2  23701  limcco  23702  dvlip  23801  dvlip2  23803  dveq0  23808  dvgt0lem1  23810  dvivthlem1  23816  dvcnvrelem1  23825  dvcnvre  23827  dvfsumlem2  23835  ftc1lem1  23843  ftc1a  23845  ftc1lem4  23847  ftc2ditglem  23853  itgsubstlem  23856  ply1rem  23968  fta1glem1  23970  ig1pdvds  23981  plyrem  24105  facth  24106  fta1lem  24107  vieta1lem1  24110  vieta1lem2  24111  aaliou3lem3  24144  aaliou3lem4  24146  aaliou3lem7  24149  taylfvallem1  24156  tayl0  24161  taylply2  24167  radcnvle  24219  psercnlem2  24223  psercnlem1  24224  psercn  24225  pserdvlem1  24226  pserdvlem2  24227  abelth2  24241  coseq00topi  24299  coseq0negpitopi  24300  cosordlem  24322  tanord1  24328  efif1olem1  24333  loglesqrt  24544  logreclem  24545  relogbval  24555  nnlogbexp  24564  chordthmlem4  24607  quart1  24628  quartlem2  24630  quartlem3  24631  quartlem4  24632  quart  24633  acosbnd  24672  atancj  24682  atanlogsublem  24687  atantan  24695  atanbndlem  24697  dvatan  24707  atantayl  24709  rlimcnp2  24738  divsqrtsumlem  24751  ftalem5  24848  ftalem7  24850  basellem4  24855  basellem5  24856  perfectlem2  25000  dchrinv  25031  chpdifbndlem1  25287  pntibndlem2  25325  pntlemc  25329  pntlema  25330  pntlemb  25331  pntlemg  25332  pntlemh  25333  pntlemq  25335  pntlemr  25336  pntlemj  25337  pntlemi  25338  pntlemf  25339  pntlemk  25340  pntlemo  25341  pntleme  25342  pntlem3  25343  pntleml  25345  abvcxp  25349  axtgpasch  25411  cgr3simp2  25461  legso  25539  hlne2  25546  hlln  25547  mirhl  25619  hlperpnel  25662  opphllem4  25687  inagswap  25775  subumgredg2  26222  upgrres1  26250  nb3grprlem1  26326  wlkp  26568  wspthsswwlkn  26883  2wlkdlem6  26896  clwwisshclwwsn  26973  erclwwlkeqlen  26976  erclwwlksym  26978  erclwwlktr  26979  clwwlkn  26985  clwwlknwrd  26996  clwwlknonex2e  27085  extwwlkfablem1OLD  27323  grpoass  27485  vcsm  27545  nvf  27643  ssps  27713  minvecolem2  27859  minvecolem4c  27863  minvecolem4  27864  minvecolem5  27865  minvecolem6  27866  eigvec1  28949  eliccelico  29667  elicoelioo  29668  slmdvsdi  29896  slmdvs1  29901  pmtrto1cl  29977  cnre2csqlem  30084  lmxrge0  30126  sigaclci  30323  difelsiga  30324  insiga  30328  ldsysgenld  30351  sigapildsyslem  30352  sigapildsys  30353  ldgenpisyslem1  30354  measvnul  30397  sibfrn  30527  eulerpartlemt  30561  eulerpartlemmf  30565  tg5segofs  30879  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem4  31291  subfacp1lem5  31292  sconnpht2  31346  sconnpi1  31347  resconn  31354  cvmsss  31375  cvmsn0  31376  cvmlift2lem3  31413  cvmlift2lem7  31417  cvmliftphtlem  31425  cvmliftpht  31426  cvmlift3lem5  31431  cvmlift3lem6  31432  msrf  31565  elmsta  31571  mclsax  31592  mthmpps  31605  mclspps  31607  scutun12  32042  slerec  32048  ivthALT  32455  poimirlem17  33556  poimirlem20  33559  ibladdnc  33597  iblabsnclem  33603  ftc1cnnclem  33613  ftc1anc  33623  ftc2nc  33624  heiborlem3  33742  iccbnd  33769  rngohom1  33897  idl0cl  33947  maxidlnr  33971  lshpne  34587  opococ  34800  opexmid  34812  hlclat  34963  lclkrslem2  37144  gneispacern2  38754  cvgdvgrat  38829  iccshift  40062  iccsuble  40063  icoiccdif  40068  mullimc  40166  limccog  40170  mullimcf  40173  lptioo2  40181  limcmptdm  40185  limcicciooub  40187  xlimmnfvlem1  40376  xlimpnfvlem1  40380  icccncfext  40418  cncfioobdlem  40427  ditgeqiooicc  40494  itgsubsticc  40510  iblcncfioo  40512  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem11  40546  stoweidlem31  40566  stoweidlem36  40571  stoweidlem38  40573  stoweidlem44  40579  stoweidlem62  40597  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem26  40668  fourierdlem32  40674  fourierdlem33  40675  fourierdlem37  40679  fourierdlem42  40684  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem69  40710  fourierdlem74  40715  fourierdlem75  40716  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem93  40734  fourierdlem101  40742  fourierdlem111  40752  saldifcl  40857  unisalgen2  40890  hoidmv1lelem3  41128  smff  41262  smfpimltxr  41277  sigardiv  41371  sigarcol  41374  sharhght  41375  sigaradd  41376  cevathlem1  41377  cevathlem2  41378  cevath  41379  proththd  41856  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator