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

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

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 898 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 263 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3simpb  913  3simpc  914  simp1  915  simp2  916  3adant3  935  3adantl3  1073  3adantr3  1076  opprc  3597  oprcl  3600  opm  3998  funtpg  4977  ftpg  5374  ovig  5649  prltlu  6642  mullocpr  6726  lt2halves  8216  nn0n0n1ge2  8368  ixxssixx  8871  dvdsmulcr  10136  dvds2add  10140  dvds2sub  10141  dvdstr  10143  bj-peano4  10446
  Copyright terms: Public domain W3C validator