Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpimim Structured version   Visualization version   GIF version

Theorem ifpimim 40710
Description: Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
Assertion
Ref Expression
ifpimim (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))

Proof of Theorem ifpimim
StepHypRef Expression
1 pm2.521 179 . . . . . 6 (¬ (¬ 𝜑𝜑) → (𝜑 → ¬ 𝜑))
21orim1i 909 . . . . 5 ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
32adantr 484 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
4 id 22 . . . . . 6 (𝜑𝜑)
54orci 864 . . . . 5 ((𝜑𝜑) ∨ (𝜃𝜒))
65a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜃𝜒)))
73, 6jca 515 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))))
84orci 864 . . . . 5 ((𝜑𝜑) ∨ (𝜓𝜏))
98a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜓𝜏)))
10 simpr 488 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))
119, 10jca 515 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
127, 11jca 515 . 2 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
13 pm4.81 397 . . . . 5 ((¬ 𝜑𝜑) ↔ 𝜑)
1413bicomi 227 . . . 4 (𝜑 ↔ (¬ 𝜑𝜑))
15 ifpbi1 40678 . . . 4 ((𝜑 ↔ (¬ 𝜑𝜑)) → (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏))))
1614, 15ax-mp 5 . . 3 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)))
17 dfifp4 1066 . . 3 (if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
1816, 17bitri 278 . 2 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
19 ifpim123g 40701 . 2 ((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
2012, 18, 193imtr4i 295 1 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  if-wif 1062
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-an 400  df-or 847  df-ifp 1063
This theorem is referenced by:  frege58acor  41070  frege60a  41072  frege65a  41077
  Copyright terms: Public domain W3C validator