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 217 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 206  df-or 846  df-3or 1085
This theorem is referenced by:  3mix3i  1332  3mix3d  1335  3jaobOLD  1424  tppreqb  4814  tpres  7220  onzsl  7858  sornom  10322  fpwwe2lem12  10687  nn0le2is012  12680  nn01to3  12979  qbtwnxr  13235  hash1to3  14512  swrdnd0  14667  pfxnd  14697  cshwshashlem1  17100  ostth  27671  nolesgn2o  27704  sltsolem1  27708  nosep2o  27715  btwncolinear1  35895  tpid3gVD  44536  limcicciooub  45276  dfxlim2v  45486
  Copyright terms: Public domain W3C validator