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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 110 . 2 ((𝜑𝜓) → 𝜓)
213ad2ant1 1019 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  simpl1r  1050  simpr1r  1056  simp11r  1110  simp21r  1116  simp31r  1122  vtoclgft  2799  en2lp  4565  funprg  5278  nnsucsssuc  6507  ecopovtrn  6646  ecopovtrng  6649  addassnqg  7395  distrnqg  7400  ltsonq  7411  ltanqg  7413  ltmnqg  7414  distrnq0  7472  addassnq0  7475  prarloclem5  7513  recexprlem1ssl  7646  recexprlem1ssu  7647  mulasssrg  7771  distrsrg  7772  lttrsr  7775  ltsosr  7777  ltasrg  7783  mulextsr1lem  7793  mulextsr1  7794  axmulass  7886  axdistr  7887  dmdcanap  8693  lt2msq1  8856  lediv2  8862  xaddass2  9884  xlt2add  9894  modqdi  10406  expaddzaplem  10577  expaddzap  10578  expmulzap  10580  bdtrilem  11261  xrbdtri  11298  prmexpb  12165  mgmsscl  12799  subgabl  13167  cnptoprest  14035  ssblps  14221  ssbl  14222  rplogbchbase  14664  rplogbreexp  14667  relogbcxpbap  14679  lgssq  14737
  Copyright terms: Public domain W3C validator