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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 109 . 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:  simpl1r  1018  simpr1r  1024  simp11r  1078  simp21r  1084  simp31r  1090  vtoclgft  2710  en2lp  4439  funprg  5143  nnsucsssuc  6356  ecopovtrn  6494  ecopovtrng  6497  addassnqg  7158  distrnqg  7163  ltsonq  7174  ltanqg  7176  ltmnqg  7177  distrnq0  7235  addassnq0  7238  prarloclem5  7276  recexprlem1ssl  7409  recexprlem1ssu  7410  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltsosr  7540  ltasrg  7546  mulextsr1lem  7556  mulextsr1  7557  axmulass  7649  axdistr  7650  dmdcanap  8450  lt2msq1  8611  lediv2  8617  xaddass2  9621  xlt2add  9631  modqdi  10133  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  bdtrilem  10978  xrbdtri  11013  prmexpb  11756  cnptoprest  12335  ssblps  12521  ssbl  12522
  Copyright terms: Public domain W3C validator