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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 107 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 962 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:  simpl1l  992  simpr1l  998  simp11l  1052  simp21l  1058  simp31l  1064  en2lp  4343  tfisi  4375  funprg  5029  nnsucsssuc  6207  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  distrnqg  6890  ltsonq  6901  ltanqg  6903  ltmnqg  6904  distrnq0  6962  addassnq0  6965  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  dmdcanap  8128  lt2msq1  8281  ltdiv2  8283  lediv2  8287  modqdi  9727  expaddzaplem  9896  expaddzap  9897  expmulzap  9899  resqrtcl  10357  prmexpb  11005
  Copyright terms: Public domain W3C validator