Metamath Proof Explorer

Theorem ifpimim

Description: Consequnce of implication. (Contributed by RP, 17-Apr-2020)

Ref Expression
Assertion ifpimim ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 pm2.521 ⊢ ( ¬ ( ¬ 𝜑 → 𝜑 ) → ( 𝜑 → ¬ 𝜑 ) )
2 1 orim1i ⊢ ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) )
3 2 adantr ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) )
4 id ⊢ ( 𝜑 → 𝜑 )
5 4 orci ⊢ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) )
6 5 a1i ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) )
7 3 6 jca ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) )
8 4 orci ⊢ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) )
9 8 a1i ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) )
10 simpr ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) )
11 9 10 jca ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) )
12 7 11 jca ⊢ ( ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) → ( ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) ) )
13 pm4.81 ⊢ ( ( ¬ 𝜑 → 𝜑 ) ↔ 𝜑 )
14 13 bicomi ⊢ ( 𝜑 ↔ ( ¬ 𝜑 → 𝜑 ) )
15 ifpbi1 ⊢ ( ( 𝜑 ↔ ( ¬ 𝜑 → 𝜑 ) ) → ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ if- ( ( ¬ 𝜑 → 𝜑 ) , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ) )
16 14 15 ax-mp ⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ if- ( ( ¬ 𝜑 → 𝜑 ) , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) )
17 dfifp4 ⊢ ( if- ( ( ¬ 𝜑 → 𝜑 ) , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) )
18 16 17 bitri ⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) ↔ ( ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) )
19 ifpim123g ⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜑 ) ∨ ( 𝜓 → 𝜒 ) ) ∧ ( ( 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜒 ) ) ) ∧ ( ( ( 𝜑 → 𝜑 ) ∨ ( 𝜓 → 𝜏 ) ) ∧ ( ( ¬ 𝜑 → 𝜑 ) ∨ ( 𝜃 → 𝜏 ) ) ) ) )
20 12 18 19 3imtr4i ⊢ ( if- ( 𝜑 , ( 𝜓 → 𝜒 ) , ( 𝜃 → 𝜏 ) ) → ( if- ( 𝜑 , 𝜓 , 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )