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

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

Proof of Theorem 3mix3
StepHypRef Expression
1 3mix1 1412 . 2 (𝜑 → (𝜑𝜓𝜒))
2 3orrot 1077 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
31, 2sylib 208 1 (𝜑 → (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071
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 197  df-or 384  df-3or 1073
This theorem is referenced by:  3mix3i  1417  3mix3d  1420  3jaob  1531  tppreqb  4473  tpres  6622  onzsl  7203  sornom  9283  fpwwe2lem13  9648  nn0le2is012  11625  nn01to3  11966  qbtwnxr  12216  hash1to3  13457  cshwshashlem1  15996  ostth  25519  nolesgn2o  32122  sltsolem1  32124  btwncolinear1  32474  tpid3gVD  39568  limcicciooub  40364  dfxlim2v  40568  pfxnd  41897
  Copyright terms: Public domain W3C validator