ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simp2 GIF version

Theorem simp2 982
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp2 ((𝜑𝜓𝜒) → 𝜓)

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 978 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simprd 113 1 ((𝜑𝜓𝜒) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simpl2  985  simpr2  988  simp2i  991  simp2d  994  simp12  1012  simp22  1015  simp32  1018  syld3an3  1261  3ianorr  1287  stoic4b  1409  nlim0  4316  tfisi  4501  sotri2  4936  sotri3  4937  feq123  5264  sefvex  5442  fvmptt  5512  fnfvima  5652  cocan1  5688  cocan2  5689  ovexg  5805  ovmpox  5899  ovmpoga  5900  caovimo  5964  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfrcllembxssdm  6253  tfrcllembfn  6254  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  mapxpen  6742  dif1en  6773  diffifi  6788  unsnfidcex  6808  unfidisj  6810  undifdc  6812  resfnfinfinss  6828  funrnfi  6830  sbthlemi9  6853  elfir  6861  difinfsn  6985  ctssdc  6998  djuassen  7073  xpdjuen  7074  mulcanenq  7200  ltanqg  7215  mulcanenq0ec  7260  addnnnq0  7264  distrprg  7403  aptipr  7456  addsrpr  7560  mulsrpr  7561  mulasssrg  7573  ltpsrprg  7618  axmulass  7688  axpre-ltadd  7701  subadd2  7973  nppcan  7991  nppcan3  7993  subsub2  7997  subsub4  8002  npncan3  8007  pnpcan  8008  pnncan  8010  subcan  8024  ltadd1  8198  leadd1  8199  leadd2  8200  ltsubadd  8201  ltsubadd2  8202  lesubadd  8203  lesubadd2  8204  ltaddsub  8205  leaddsub  8207  lesub1  8225  lesub2  8226  ltsub1  8227  ltsub2  8228  gt0add  8342  apreap  8356  lemul1  8362  reapmul1lem  8363  reapmul1  8364  reapadd1  8365  remulext1  8368  remulext2  8369  apadd2  8378  mulext2  8382  mulap0r  8384  leltap  8394  ltap  8402  apsub1  8411  recexaplem2  8420  mulcanap  8433  mulcanap2  8434  divvalap  8441  divmulap  8442  divcanap1  8448  diveqap0  8449  divap0b  8450  divrecap  8455  divassap  8457  div23ap  8458  divdirap  8464  divcanap3  8465  div11ap  8467  diveqap1  8472  divmuldivap  8479  divcanap5  8481  redivclap  8498  div2negap  8502  apmul1  8555  apmul2  8556  div2subap  8603  ltdiv1  8633  ledivmul  8642  lemuldiv  8646  lt2msq1  8650  ltdiv23  8657  squeeze0  8669  zaddcllemneg  9100  eluzsub  9362  nn01to3  9416  rpgecl  9477  addlelt  9562  xleadd1  9665  xltadd1  9666  lbioog  9703  ubioc1  9719  ubicc2  9775  icoshftf1o  9781  fzen  9830  ubmelfzo  9984  ssfzo12  10008  ubmelm1fzo  10010  fzosplitprm1  10018  rebtwn2zlemshrink  10038  qbtwnre  10041  flqwordi  10068  flqword2  10069  flltdivnn0lt  10084  modqcl  10106  mulqmod0  10110  modqmulnn  10122  modqabs2  10138  modqmuladdnn0  10148  qnegmod  10149  addmodid  10152  modqm1p1mod0  10155  modifeq2int  10166  modqdi  10172  modqeqmodmin  10174  modfzo0difsn  10175  frec2uzf1od  10186  exp3val  10302  expnegap0  10308  expgt1  10338  exprecap  10341  expmulzap  10346  leexp2a  10353  expubnd  10357  mulbinom2  10415  bernneq2  10420  expnbnd  10422  fihashss  10569  fihashssdif  10571  fimaxq  10580  shftuz  10596  shftfibg  10599  cjdivap  10688  resqrtcl  10808  absdivap  10849  abssubne0  10870  maxleast  10992  lemininf  11012  ltmininf  11013  xrmaxltsup  11034  xrmaxaddlem  11036  xrmaxadd  11037  xrmineqinf  11045  xrltmininf  11046  xrminltinf  11048  xrminadd  11051  climuni  11069  reccn2ap  11089  isumz  11165  geoisum1c  11296  efltim  11411  dvdsval2  11503  dvdscmulr  11529  dvdsmulcr  11530  modmulconst  11532  dvdsadd2b  11547  dvdsexp  11566  mulmoddvds  11568  divalglemeuneg  11627  gcdaddm  11679  dvdsgcdb  11708  mulgcd  11711  gcddiv  11714  lcmdvdsb  11772  mulgcddvds  11782  qredeq  11784  divgcdcoprm0  11789  cncongr1  11791  euclemma  11831  rpexp  11838  rpexp12i  11840  ctinf  11950  fvsetsid  12003  ressid2  12028  ressval2  12029  rngplusgg  12086  2basgeng  12261  iuncld  12294  ntrss  12298  restco  12353  restabs  12354  cnprcl2k  12385  lmconst  12395  cnrest2  12415  cnmpt2t  12472  psmetsym  12508  psmetge0  12510  xmetge0  12544  xmetsym  12547  blvalps  12567  blval  12568  xblcntrps  12592  xblcntr  12593  xmssym  12648  blsscls2  12672  bdxmet  12680  txmetcnp  12697  dvfvalap  12829  dvid  12841  dvcnp2cntop  12842  findset  13173
  Copyright terms: Public domain W3C validator