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

Theorem 3simpc 938
 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 925 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
2 3simpa 936 . 2 ((𝜓𝜒𝜑) → (𝜓𝜒))
31, 2sylbi 119 1 ((𝜑𝜓𝜒) → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 920 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115  df-3an 922 This theorem is referenced by:  simp3  941  3adant1  957  3adantl1  1095  3adantr1  1098  eupickb  2023  find  4342  eqsupti  6458  divcanap2  7824  diveqap0  7826  divrecap  7832  divcanap3  7842  eliooord  9016  fzrev3  9169  sqdivap  9626  muldvds2  10355  dvdscmul  10356  dvdsmulc  10357  dvdstr  10366
 Copyright terms: Public domain W3C validator