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

Theorem simplll 500
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplll ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simplll
StepHypRef Expression
1 simpl 107 . 2 ((𝜑𝜓) → 𝜑)
21ad2antrr 472 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simp-4l  508  f1imass  5445  tfrlem1  5957  phplem4dom  6397  phplem4on  6402  suplub2ti  6473  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  ltexnqq  6660  enq0tr  6686  addcmpblnq0  6695  mulcmpblnq0  6696  nnnq0lem1  6698  prssnql  6731  prmuloc  6818  prmuloc2  6819  mullocpr  6823  ltexprlemopu  6855  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  ltmprr  6894  archpr  6895  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  ltsrprg  6986  srpospr  7021  axcaucvglemres  7127  negeu  7366  add20  7645  rimul  7752  apreap  7754  cru  7769  mulge0  7786  mulap0  7811  prodgt0  7997  ltmul12a  8005  ledivdiv  8035  lediv12a  8039  qapne  8805  qreccl  8808  ixxss12  9005  ioodisj  9091  fznlem  9136  elfz0fzfz0  9214  btwnzge0  9382  mulexpzap  9613  leexp1a  9628  expnbnd  9693  sizeennnuni  9803  resqrexlemga  10047  sqrtsq  10068  abs3lem  10135  cau3lem  10138  minmax  10250  climcau  10322  dvdsle  10389  gcdsupex  10493  gcdsupcl  10494  bezoutlemmain  10531  bezoutlemzz  10535  dfgcd3  10543  dvdsmulgcd  10558  lcmcllem  10593  lcmgcdlem  10603  ncoprmgcdne1b  10615  qredeu  10623  oddpwdclemxy  10691  oddpwdclemdc  10695
  Copyright terms: Public domain W3C validator