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

Theorem 3simpa 961
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3simpa ((𝜑𝜓𝜒) → (𝜑𝜓))

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 947 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 270 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3simpb  962  3simpc  963  simp1  964  simp2  965  3adant3  984  3adantl3  1122  3adantr3  1125  opprc  3694  oprcl  3697  opm  4124  funtpg  5142  ftpg  5570  ovig  5858  prltlu  7259  mullocpr  7343  lt2halves  8906  nn0n0n1ge2  9072  ixxssixx  9625  sumtp  11123  dvdsmulcr  11419  dvds2add  11423  dvds2sub  11424  dvdstr  11426  bj-peano4  12964
  Copyright terms: Public domain W3C validator