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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 108 . 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:  simpl1r  993  simpr1r  999  simp11r  1053  simp21r  1059  simp31r  1065  vtoclgft  2663  en2lp  4343  funprg  5029  nnsucsssuc  6207  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  distrnqg  6890  ltsonq  6901  ltanqg  6903  ltmnqg  6904  distrnq0  6962  addassnq0  6965  prarloclem5  7003  recexprlem1ssl  7136  recexprlem1ssu  7137  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  dmdcanap  8128  lt2msq1  8281  lediv2  8287  modqdi  9727  expaddzaplem  9897  expaddzap  9898  expmulzap  9900  prmexpb  11012
  Copyright terms: Public domain W3C validator