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

Theorem simp3l 969
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 107 . 2 ((𝜒𝜃) → 𝜒)
213ad2ant3 964 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  simpl3l  996  simpr3l  1002  simp13l  1056  simp23l  1062  simp33l  1068  issod  4120  tfisi  4375  tfrlem5  6033  tfrlemibxssdm  6046  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  ltsonq  6901  ltanqg  6903  ltmnqg  6904  addassnq0  6965  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  lemul1  8011  reapmul1lem  8012  reapmul1  8013  mulcanap  8073  mulcanap2  8074  divassap  8096  divdirap  8103  div11ap  8106  muldivdirap  8113  divcanap5  8120  apmul1  8194  ltdiv1  8264  ltmuldiv  8270  ledivmul  8273  lemuldiv  8277  ltdiv2  8283  lediv2  8287  ltdiv23  8288  lediv23  8289  modqdi  9727  expaddzap  9897  expmulzap  9899  leisorel  10138  resqrtcl  10357  dvdscmulr  10700  dvdsmulcr  10701  dvdsadd2b  10718  dvdsgcd  10876  rpexp12i  11009
  Copyright terms: Public domain W3C validator