MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3mix3 Structured version   Visualization version   GIF version

Theorem 3mix3 1329
Description: Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3mix3 (𝜑 → (𝜓𝜒𝜑))

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1327 . 2 (𝜑 → (𝜑𝜓𝜒))
2 3orrot 1089 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
31, 2sylib 221 1 (𝜑 → (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-or 845  df-3or 1085
This theorem is referenced by:  3mix3i  1332  3mix3d  1335  3jaob  1423  tppreqb  4722  tpres  6954  onzsl  7555  sornom  9697  fpwwe2lem13  10062  nn0le2is012  12043  nn01to3  12338  qbtwnxr  12590  hash1to3  13854  swrdnd0  14019  pfxnd  14049  cshwshashlem1  16429  ostth  26229  nolesgn2o  33238  sltsolem1  33240  btwncolinear1  33590  tpid3gVD  41472  limcicciooub  42209  dfxlim2v  42419
  Copyright terms: Public domain W3C validator