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- φ χ τ