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 38394
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 167 . . . . . 6 (¬ (¬ 𝜑𝜑) → (𝜑 → ¬ 𝜑))
21orim1i 922 . . . . 5 ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
32adantr 467 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
4 id 22 . . . . . 6 (𝜑𝜑)
54orci 881 . . . . 5 ((𝜑𝜑) ∨ (𝜃𝜒))
65a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜃𝜒)))
73, 6jca 502 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))))
84orci 881 . . . . 5 ((𝜑𝜑) ∨ (𝜓𝜏))
98a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜓𝜏)))
10 simpr 472 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))
119, 10jca 502 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
127, 11jca 502 . 2 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
13 pm4.81 381 . . . . 5 ((¬ 𝜑𝜑) ↔ 𝜑)
1413bicomi 215 . . . 4 (𝜑 ↔ (¬ 𝜑𝜑))
15 ifpbi1 38362 . . . 4 ((𝜑 ↔ (¬ 𝜑𝜑)) → (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏))))
1614, 15ax-mp 5 . . 3 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)))
17 dfifp4 1080 . . 3 (if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
1816, 17bitri 265 . 2 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
19 ifpim123g 38385 . 2 ((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
2012, 18, 193imtr4i 282 1 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  wo 863  if-wif 1076
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 198  df-an 384  df-or 864  df-ifp 1077
This theorem is referenced by:  frege58acor  38710  frege60a  38712  frege65a  38717
  Copyright terms: Public domain W3C validator