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

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

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 965 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 272 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963 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 965 This theorem is referenced by:  3simpb  980  3simpc  981  simp1  982  simp2  983  3adant3  1002  3adantl3  1140  3adantr3  1143  opprc  3762  oprcl  3765  opm  4194  funtpg  5220  ftpg  5650  ovig  5939  prltlu  7401  mullocpr  7485  lt2halves  9062  nn0n0n1ge2  9228  ixxssixx  9799  sumtp  11304  dvdsmulcr  11709  dvds2add  11713  dvds2sub  11714  dvdstr  11716  bj-peano4  13501
 Copyright terms: Public domain W3C validator