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  5508  tfrlem1  6021  phplem4dom  6524  phplem4on  6529  fisseneq  6586  suplub2ti  6633  addcmpblnq  6863  mulcmpblnq  6864  ordpipqqs  6870  ltexnqq  6904  enq0tr  6930  addcmpblnq0  6939  mulcmpblnq0  6940  nnnq0lem1  6942  prssnql  6975  prmuloc  7062  prmuloc2  7063  mullocpr  7067  ltexprlemopu  7099  ltexprlemrl  7106  ltexprlemru  7108  addcanprleml  7110  addcanprlemu  7111  ltmprr  7138  archpr  7139  addcmpblnr  7222  mulcmpblnrlemg  7223  mulcmpblnr  7224  ltsrprg  7230  srpospr  7265  axcaucvglemres  7371  negeu  7610  add20  7889  rimul  7996  apreap  7998  cru  8013  mulge0  8030  mulap0  8055  prodgt0  8241  ltmul12a  8249  ledivdiv  8279  lediv12a  8283  qapne  9049  qreccl  9052  ixxss12  9249  ioodisj  9335  fznlem  9380  elfz0fzfz0  9458  btwnzge0  9628  mulexpzap  9886  leexp1a  9901  expnbnd  9966  hashennnuni  10076  zfz1iso  10135  iseqcoll  10136  resqrexlemga  10344  sqrtsq  10365  abs3lem  10432  cau3lem  10435  minmax  10547  climcau  10619  isummolem2  10654  dvdsle  10712  gcdsupex  10816  gcdsupcl  10817  bezoutlemmain  10854  bezoutlemzz  10858  dfgcd3  10866  dvdsmulgcd  10881  lcmcllem  10916  lcmgcdlem  10926  ncoprmgcdne1b  10938  qredeu  10946  oddpwdclemxy  11014  oddpwdclemdc  11018  nninfalllemn  11328  nninfalllem1  11329
  Copyright terms: Public domain W3C validator