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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 107 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 934 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 896
This theorem is referenced by:  simpl1r  965  simpr1r  971  simp11r  1025  simp21r  1031  simp31r  1037  vtoclgft  2619  en2lp  4303  funprg  4974  nnsucsssuc  6099  ecopovtrn  6231  ecopovtrng  6234  addassnqg  6508  distrnqg  6513  ltsonq  6524  ltanqg  6526  ltmnqg  6527  distrnq0  6585  addassnq0  6588  prarloclem5  6626  recexprlem1ssl  6759  recexprlem1ssu  6760  mulasssrg  6871  distrsrg  6872  lttrsr  6875  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892  mulextsr1  6893  axmulass  6975  axdistr  6976  dmdcanap  7743  lt2msq1  7896  lediv2  7902  modqdi  9307  expaddzaplem  9428  expaddzap  9429  expmulzap  9431
  Copyright terms: Public domain W3C validator