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

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

Proof of Theorem simplll
StepHypRef Expression
1 simpl 108 . 2 ((𝜑𝜓) → 𝜑)
21ad2antrr 480 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simp-4l  531  f1imass  5682  tfrlem1  6212  phplem4dom  6763  phplem4on  6768  fisseneq  6827  suplub2ti  6895  omp1eomlem  6986  addcmpblnq  7198  mulcmpblnq  7199  ordpipqqs  7205  ltexnqq  7239  enq0tr  7265  addcmpblnq0  7274  mulcmpblnq0  7275  nnnq0lem1  7277  prssnql  7310  prmuloc  7397  prmuloc2  7398  mullocpr  7402  ltexprlemopu  7434  ltexprlemrl  7441  ltexprlemru  7443  addcanprleml  7445  addcanprlemu  7446  ltmprr  7473  archpr  7474  suplocexprlemloc  7552  addcmpblnr  7570  mulcmpblnrlemg  7571  mulcmpblnr  7572  ltsrprg  7578  srpospr  7614  axcaucvglemres  7730  axpre-suploclemres  7732  axpre-suploc  7733  negeu  7976  add20  8259  rimul  8370  apreap  8372  cru  8387  mulge0  8404  mulap0  8438  prodgt0  8633  ltmul12a  8641  ledivdiv  8671  lediv12a  8675  qapne  9457  qreccl  9460  xleaddadd  9699  ixxss12  9718  ioodisj  9805  fznlem  9851  elfz0fzfz0  9933  btwnzge0  10103  mulexpzap  10363  leexp1a  10378  expnbnd  10445  hashennnuni  10556  zfz1iso  10615  seq3coll  10616  resqrexlemga  10826  sqrtsq  10847  abs3lem  10914  cau3lem  10917  minmax  11032  xrmaxiflemval  11050  xrminmax  11065  climcau  11147  summodclem2  11182  fsumrelem  11271  cvgratz  11332  mertenslemi1  11335  mertenslem2  11336  mertensabs  11337  dvdsle  11576  gcdsupex  11680  gcdsupcl  11681  bezoutlemmain  11720  bezoutlemzz  11724  dfgcd3  11732  dvdsmulgcd  11747  lcmcllem  11782  lcmgcdlem  11792  ncoprmgcdne1b  11804  qredeu  11812  oddpwdclemxy  11881  oddpwdclemdc  11885  ctiunctlemfo  11986  unct  11989  neissex  12371  restbasg  12374  tgrest  12375  restopnb  12387  cnptopco  12428  metequiv2  12702  xmettx  12716  metcnpi3  12723  fsumcncntop  12762  elcncf2  12767  cncfmet  12785  dedekindeulemuub  12801  dedekindeulemlu  12805  dedekindicclemuub  12810  dedekindicclemlu  12814  limccnpcntop  12850  reeff1olem  12898  nninfalllemn  13375  nninfalllem1  13376  apdiff  13414
  Copyright terms: Public domain W3C validator