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

Theorem simp1r 964
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 960 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
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 922
This theorem is referenced by:  simpl1r  991  simpr1r  997  simp11r  1051  simp21r  1057  simp31r  1063  vtoclgft  2650  en2lp  4305  funprg  4980  nnsucsssuc  6136  ecopovtrn  6269  ecopovtrng  6272  addassnqg  6634  distrnqg  6639  ltsonq  6650  ltanqg  6652  ltmnqg  6653  distrnq0  6711  addassnq0  6714  prarloclem5  6752  recexprlem1ssl  6885  recexprlem1ssu  6886  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  mulextsr1lem  7018  mulextsr1  7019  axmulass  7101  axdistr  7102  dmdcanap  7877  lt2msq1  8030  lediv2  8036  modqdi  9474  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  prmexpb  10674
  Copyright terms: Public domain W3C validator