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

Theorem simp3l 932
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 927 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
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 887
This theorem is referenced by:  simpl3l  959  simpr3l  965  simp13l  1019  simp23l  1025  simp33l  1031  issod  4056  tfisi  4310  tfrlem5  5930  tfrlemibxssdm  5941  ecopovtrn  6203  ecopovtrng  6206  addassnqg  6478  ltsonq  6494  ltanqg  6496  ltmnqg  6497  addassnq0  6558  mulasssrg  6841  distrsrg  6842  lttrsr  6845  ltsosr  6847  ltasrg  6853  mulextsr1lem  6862  mulextsr1  6863  axmulass  6945  axdistr  6946  lemul1  7582  reapmul1lem  7583  reapmul1  7584  mulcanap  7644  mulcanap2  7645  divassap  7667  divdirap  7672  div11ap  7675  divcanap5  7688  apmul1  7762  ltdiv1  7832  ltmuldiv  7838  ledivmul  7841  lemuldiv  7845  ltdiv2  7851  lediv2  7855  ltdiv23  7856  lediv23  7857  expaddzap  9297  expmulzap  9299  resqrtcl  9625
  Copyright terms: Public domain W3C validator