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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 108 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 987 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
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 depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  simpl1l  1017  simpr1l  1023  simp11l  1077  simp21l  1083  simp31l  1089  en2lp  4439  tfisi  4471  funprg  5143  nnsucsssuc  6356  ecopovtrn  6494  ecopovtrng  6497  addassnqg  7158  distrnqg  7163  ltsonq  7174  ltanqg  7176  ltmnqg  7177  distrnq0  7235  addassnq0  7238  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1lem  7556  mulextsr1  7557  axmulass  7649  axdistr  7650  dmdcanap  8450  lt2msq1  8611  ltdiv2  8613  lediv2  8617  xaddass  9620  xaddass2  9621  xlt2add  9631  modqdi  10133  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  resqrtcl  10769  bdtrilem  10978  bdtri  10979  xrbdtri  11013  prmexpb  11756  cnptoprest  12335  ssblps  12521  ssbl  12522
  Copyright terms: Public domain W3C validator