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

Theorem 3simpc 981
 Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
3simpc ((𝜑𝜓𝜒) → (𝜓𝜒))

Proof of Theorem 3simpc
StepHypRef Expression
1 3anrot 968 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
2 3simpa 979 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒))
31, 2sylbi 120 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  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  simp3  984  3adant1  1000  3adantl1  1138  3adantr1  1141  eupickb  2081  find  4522  fisseneq  6830  eqsupti  6893  divcanap2  8484  diveqap0  8486  divrecap  8492  divcanap3  8502  eliooord  9761  fzrev3  9918  sqdivap  10408  muldvds2  11575  dvdscmul  11576  dvdsmulc  11577  dvdstr  11586  cncfmptc  12810  cnplimclemr  12866
 Copyright terms: Public domain W3C validator