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

Theorem simp1r 987
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 983 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 943
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 945
This theorem is referenced by:  simpl1r  1014  simpr1r  1020  simp11r  1074  simp21r  1080  simp31r  1086  vtoclgft  2705  en2lp  4427  funprg  5129  nnsucsssuc  6340  ecopovtrn  6478  ecopovtrng  6481  addassnqg  7132  distrnqg  7137  ltsonq  7148  ltanqg  7150  ltmnqg  7151  distrnq0  7209  addassnq0  7212  prarloclem5  7250  recexprlem1ssl  7383  recexprlem1ssu  7384  mulasssrg  7495  distrsrg  7496  lttrsr  7499  ltsosr  7501  ltasrg  7507  mulextsr1lem  7516  mulextsr1  7517  axmulass  7602  axdistr  7603  dmdcanap  8389  lt2msq1  8547  lediv2  8553  xaddass2  9540  xlt2add  9550  modqdi  10052  expaddzaplem  10223  expaddzap  10224  expmulzap  10226  bdtrilem  10896  xrbdtri  10931  prmexpb  11669  cnptoprest  12244  ssblps  12408  ssbl  12409
  Copyright terms: Public domain W3C validator