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

Theorem simp3l 931
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l ((φ ψ (χ θ)) → χ)

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 102 . 2 ((χ θ) → χ)
213ad2ant3 926 1 ((φ ψ (χ θ)) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simpl3l  958  simpr3l  964  simp13l  1018  simp23l  1024  simp33l  1030  issod  4047  tfisi  4253  tfrlem5  5871  tfrlemibxssdm  5882  ecopovtrn  6139  ecopovtrng  6142  addassnqg  6366  ltsonq  6382  ltanqg  6384  ltmnqg  6385  addassnq0  6444  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltsosr  6672  ltasrg  6678  mulextsr1lem  6686  mulextsr1  6687  axmulass  6737  axdistr  6738  lemul1  7357  reapmul1lem  7358  reapmul1  7359  mulcanap  7408  mulcanap2  7409  divassap  7431  divdirap  7436  div11ap  7439  divcanap5  7452  apmul1  7526  ltdiv1  7595  ltmuldiv  7601  ledivmul  7604  lemuldiv  7608  ltdiv2  7614  lediv2  7618  ltdiv23  7619  lediv23  7620  expaddzap  8933  expmulzap  8935
  Copyright terms: Public domain W3C validator