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

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

Proof of Theorem 3simpa
StepHypRef Expression
1 df-3an 980 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
21simplbi 274 1 ((𝜑𝜓𝜒) → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3simpb  995  3simpc  996  simp1  997  simp2  998  3adant3  1017  3adantl3  1155  3adantr3  1158  opprc  3797  oprcl  3800  opm  4230  funtpg  5262  ftpg  5695  ovig  5989  prltlu  7464  mullocpr  7548  lt2halves  9130  nn0n0n1ge2  9299  ixxssixx  9876  sumtp  11393  dvdsmulcr  11799  dvds2add  11803  dvds2sub  11804  dvdstr  11806  dfgrp3me  12846  bj-peano4  14329
  Copyright terms: Public domain W3C validator