Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  redundpim3 Structured version   Visualization version   GIF version

Theorem redundpim3 35857
Description: Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.)
Hypothesis
Ref Expression
redundpim3.1 (𝜃𝜒)
Assertion
Ref Expression
redundpim3 ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))

Proof of Theorem redundpim3
StepHypRef Expression
1 anbi1 633 . . . 4 (((𝜑𝜒) ↔ (𝜓𝜒)) → (((𝜑𝜒) ∧ 𝜃) ↔ ((𝜓𝜒) ∧ 𝜃)))
2 redundpim3.1 . . . . . 6 (𝜃𝜒)
32pm4.71ri 563 . . . . 5 (𝜃 ↔ (𝜒𝜃))
43bianass 640 . . . 4 ((𝜑𝜃) ↔ ((𝜑𝜒) ∧ 𝜃))
53bianass 640 . . . 4 ((𝜓𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
61, 4, 53bitr4g 316 . . 3 (((𝜑𝜒) ↔ (𝜓𝜒)) → ((𝜑𝜃) ↔ (𝜓𝜃)))
76anim2i 618 . 2 (((𝜑𝜓) ∧ ((𝜑𝜒) ↔ (𝜓𝜒))) → ((𝜑𝜓) ∧ ((𝜑𝜃) ↔ (𝜓𝜃))))
8 df-redundp 35852 . 2 ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ ((𝜑𝜒) ↔ (𝜓𝜒))))
9 df-redundp 35852 . 2 ( redund (𝜑, 𝜓, 𝜃) ↔ ((𝜑𝜓) ∧ ((𝜑𝜃) ↔ (𝜓𝜃))))
107, 8, 93imtr4i 294 1 ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   redund wredundp 35467
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 209  df-an 399  df-redundp 35852
This theorem is referenced by:  refrelredund2  35863
  Copyright terms: Public domain W3C validator