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

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

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 978 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simpld 111 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
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simpl1  984  simpr1  987  simp1i  990  simp1d  993  simp11  1011  simp21  1014  simp31  1017  syld3an3  1261  3ianorr  1287  stoic4a  1408  stoic4b  1409  rsp2e  2483  issod  4244  elirr  4459  sotri2  4939  sotri3  4940  funtpg  5177  funimaexglem  5209  feq123  5267  ftpg  5607  fsnunf  5623  foco2  5658  fcofo  5688  f1oiso2  5731  riotass  5760  ovmpox  5902  ovmpoga  5903  caovimo  5967  ofeq  5987  ofrval  5995  tfr1onlembxssdm  6243  tfrcllembxssdm  6256  frecsuclem  6306  frecrdg  6308  mapxpen  6745  diffifi  6791  unsnfidcex  6811  unsnfidcel  6812  unfidisj  6813  undifdc  6815  ssfidc  6826  iunfidisj  6837  sbthlemi9  6856  elfir  6864  djuassen  7085  mulcanenq  7212  ltanqg  7227  addnnnq0  7276  distrlem4prl  7411  distrlem4pru  7412  distrprg  7415  aptipr  7468  addsrpr  7572  mulsrpr  7573  mulasssrg  7585  ltpsrprg  7630  axmulass  7700  axpre-ltadd  7713  mul31  7912  addsubass  7991  subcan2  8006  subsub2  8009  subsub4  8014  npncan3  8019  pnpcan  8020  pnncan  8022  subcan  8036  subdi  8166  ltadd1  8210  leadd1  8211  leadd2  8212  ltsubadd  8213  lesubadd  8215  ltaddsub  8217  leaddsub  8219  lesub1  8237  lesub2  8238  ltsub1  8239  ltsub2  8240  ltaddsublt  8352  gt0add  8354  apreap  8368  lemul1  8374  reapmul1lem  8375  reapmul1  8376  reapadd1  8377  remulext1  8380  remulext2  8381  apadd2  8390  mulext2  8394  mulap0r  8396  leltap  8406  ltap  8414  apsub1  8423  recexaplem2  8432  mulcanap  8445  mulcanap2  8446  divvalap  8453  divcanap2  8459  diveqap0  8461  divrecap  8467  divrecap2  8468  divdirap  8476  divcanap3  8477  div11ap  8479  muldivdirap  8486  divcanap5  8493  redivclap  8510  div2negap  8514  apmul1  8567  apmul2  8568  div2subap  8615  ltdiv1  8645  ltmuldiv  8651  lemuldiv  8658  lt2msq1  8662  ltdiv23  8669  lediv23  8670  squeeze0  8681  gtndiv  9165  eluz2  9351  eluzsub  9374  peano2uz  9400  nn01to3  9431  divge1  9533  ledivge1le  9536  addlelt  9578  xaddass  9675  xleadd1  9681  xltadd1  9682  ixxssixx  9708  lbico1  9736  lbicc2  9790  icoshftf1o  9797  fzen  9847  fzrev3  9891  fzrevral2  9910  elfzo0  9983  elfzo0z  9985  fzosplitprm1  10035  qbtwnre  10058  flqwordi  10085  flqword2  10086  adddivflid  10089  flltdivnn0lt  10101  modqcl  10123  mulqmod0  10127  modqmulnn  10139  modqabs2  10155  addmodid  10169  modifeq2int  10183  modqeqmodmin  10191  seqeq2  10246  seqeq3  10247  exp3val  10319  expnegap0  10325  expgt1  10355  exprecap  10358  leexp2a  10370  expubnd  10374  sqdivap  10381  expnbnd  10439  bccmpl  10524  fihashss  10586  leisorel  10604  shftfibg  10616  mulreap  10660  abssubne0  10887  maxleast  11009  lemininf  11029  ltmininf  11030  xrmaxltsup  11051  xrmaxaddlem  11053  xrmaxadd  11054  xrmineqinf  11062  xrltmininf  11063  xrminltinf  11065  xrminadd  11068  climuni  11086  reccn2ap  11106  isumz  11182  fsumsplitsnun  11212  geoisum1c  11313  efltim  11428  dvdscmulr  11545  dvdsmulcr  11546  summodnegmod  11547  modmulconst  11548  dvdsmultr2  11556  dvdsexp  11582  mulmoddvds  11584  modremain  11649  divgcdz  11683  gcdaddm  11695  dvdsgcdb  11724  gcdass  11726  mulgcd  11727  gcddiv  11730  rplpwr  11738  lcmdvdsb  11788  lcmass  11789  mulgcddvds  11798  qredeq  11800  qredeu  11801  rpmul  11802  divgcdcoprmex  11806  cncongr1  11807  rpexp  11854  rpexp12i  11856  ctinf  11966  setsvala  12016  ressid2  12044  ressval2  12045  rngbaseg  12101  2basgeng  12277  clsss  12313  ntrss  12314  ntrin  12319  neiss  12345  restco  12369  restabs  12370  lmconst  12411  psmetsym  12524  psmetge0  12526  xmetge0  12560  xmetsym  12563  xmetresbl  12635  mopni3  12679  bdxmet  12696  bdmopn  12699  txmetcnp  12713  dvfvalap  12845  dvid  12857  dvcnp2cntop  12858  ptolemy  12939  rpcxpadd  13020  rpmulcxp  13024  rpdivcxp  13026  cxpmul  13027  rpcxple2  13032  rpcxplt2  13033  cxpcom  13051  rplogbval  13055  rplogbcl  13056  rprelogbmulexp  13066  relogbexpap  13068  logbleb  13071  logblt  13072  rplogbcxp  13073  rpcxplogb  13074
  Copyright terms: Public domain W3C validator