ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simp-4r GIF version

Theorem simp-4r 542
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-4r (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r
StepHypRef Expression
1 simpllr 534 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
21adantr 276 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
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 is referenced by:  simp-5r  544  fimax2gtri  6929  finexdc  6930  dcfi  7010  difinfsn  7129  nnnninfeq2  7157  nninfisol  7161  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  suplocexprlemru  7748  suplocsrlemb  7835  suplocsrlem  7837  aptap  8637  supinfneg  9625  infsupneg  9626  xaddf  9874  xaddval  9875  nn0ltexp2  10721  hashunlem  10816  xrmaxiflemcl  11285  xrmaxiflemlub  11288  xrmaxltsup  11298  sumeq2  11399  fsumconst  11494  prodeq2  11597  fprodconst  11660  sgrpidmndm  12881  mhmmnd  13058  ghmcmn  13265  issrg  13319  cncnp  14187  neitx  14225  dedekindeulemlu  14556  suplociccreex  14559  dedekindicclemlu  14565  cnplimclemr  14595  limccnp2cntop  14603  logbgcd1irrap  14845  lgsval  14863
  Copyright terms: Public domain W3C validator