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

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

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 901 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simpld 105 1 ((𝜑𝜓𝜒) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  simpl1  907  simpr1  910  simp1i  913  simp1d  916  simp11  934  simp21  937  simp31  940  syld3an3  1180  3ianorr  1204  stoic4a  1321  stoic4b  1322  rsp2e  2372  issod  4056  elirr  4266  sotri2  4722  sotri3  4723  funtpg  4950  funimaexglem  4982  feq123  5038  foco2  5318  ftpg  5347  fsnunf  5362  fcofo  5424  f1oiso2  5466  riotass  5495  ovmpt2x  5629  ovmpt2ga  5630  caovimo  5694  ofeq  5714  ofrval  5722  frecsuclem3  5990  diffifi  6351  mulcanenq  6481  ltanqg  6496  addnnnq0  6545  distrlem4prl  6680  distrlem4pru  6681  distrprg  6684  aptipr  6737  addsrpr  6828  mulsrpr  6829  mulasssrg  6841  axmulass  6945  axpre-ltadd  6958  mul31  7142  addsubass  7219  subcan2  7234  subsub2  7237  subsub4  7242  npncan3  7247  pnpcan  7248  pnncan  7250  subcan  7264  subdi  7380  ltadd1  7422  leadd1  7423  leadd2  7424  ltsubadd  7425  lesubadd  7427  ltaddsub  7429  leaddsub  7431  lesub1  7449  lesub2  7450  ltsub1  7451  ltsub2  7452  ltaddsublt  7560  gt0add  7562  apreap  7576  lemul1  7582  reapmul1lem  7583  reapmul1  7584  reapadd1  7585  remulext1  7588  remulext2  7589  apadd2  7598  mulext2  7602  mulap0r  7604  leltap  7613  ltap  7620  recexaplem2  7631  mulcanap  7644  mulcanap2  7645  divvalap  7651  divcanap2  7657  diveqap0  7659  divrecap  7665  divrecap2  7666  divdirap  7672  divcanap3  7673  div11ap  7675  divcanap5  7688  redivclap  7705  div2negap  7709  apmul1  7762  ltdiv1  7832  ltmuldiv  7838  lemuldiv  7845  lt2msq1  7849  ltdiv23  7856  lediv23  7857  squeeze0  7868  gtndiv  8333  eluz2  8477  eluzsub  8500  peano2uz  8524  nn01to3  8550  divge1  8647  ledivge1le  8650  ixxssixx  8769  lbico1  8797  lbicc2  8850  icoshftf1o  8857  fzen  8905  fzrev3  8947  fzrevral2  8966  elfzo0  9036  elfzo0z  9038  fzosplitprm1  9088  qbtwnre  9109  flqwordi  9128  flqword2  9129  adddivflid  9132  flltdivnn0lt  9144  modqcl  9166  mulqmod0  9170  modqmulnn  9182  iseqeq2  9213  iseqeq3  9214  expnegap0  9261  expgt1  9291  exprecap  9294  leexp2a  9305  expubnd  9309  sqdivap  9316  expnbnd  9370  shftfibg  9419  mulreap  9462  abssubne0  9685  climuni  9812
  Copyright terms: Public domain W3C validator