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 37370
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 166 . . . . . 6 (¬ (¬ 𝜑𝜑) → (𝜑 → ¬ 𝜑))
21orim1i 539 . . . . 5 ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
32adantr 481 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)))
4 id 22 . . . . . 6 (𝜑𝜑)
54orci 405 . . . . 5 ((𝜑𝜑) ∨ (𝜃𝜒))
65a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜃𝜒)))
73, 6jca 554 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))))
84orci 405 . . . . 5 ((𝜑𝜑) ∨ (𝜓𝜏))
98a1i 11 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((𝜑𝜑) ∨ (𝜓𝜏)))
10 simpr 477 . . . 4 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))
119, 10jca 554 . . 3 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
127, 11jca 554 . 2 (((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))) → ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
13 pm4.81 381 . . . . 5 ((¬ 𝜑𝜑) ↔ 𝜑)
1413bicomi 214 . . . 4 (𝜑 ↔ (¬ 𝜑𝜑))
15 ifpbi1 37338 . . . 4 ((𝜑 ↔ (¬ 𝜑𝜑)) → (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏))))
1614, 15ax-mp 5 . . 3 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)))
17 dfifp4 1015 . . 3 (if-((¬ 𝜑𝜑), (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
1816, 17bitri 264 . 2 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) ↔ ((¬ (¬ 𝜑𝜑) ∨ (𝜓𝜒)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏))))
19 ifpim123g 37361 . 2 ((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓𝜒)) ∧ ((𝜑𝜑) ∨ (𝜃𝜒))) ∧ (((𝜑𝜑) ∨ (𝜓𝜏)) ∧ ((¬ 𝜑𝜑) ∨ (𝜃𝜏)))))
2012, 18, 193imtr4i 281 1 (if-(𝜑, (𝜓𝜒), (𝜃𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  if-wif 1011
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 385  df-an 386  df-ifp 1012
This theorem is referenced by:  frege58acor  37687  frege60a  37689  frege65a  37694
  Copyright terms: Public domain W3C validator