Metamath Proof Explorer

Theorem antnestlaw2

Description: A law of nested antecedents. (Contributed by Adrian Ducourtial, 5-Dec-2025)

Ref Expression
Assertion antnestlaw2 
|- ( ( ( ( ph -> ps ) -> ps ) -> ch ) <-> ( ( ( ph -> ch ) -> ps ) -> ch ) )

Proof

Step Hyp Ref Expression
1 pm2.27 
 |-  ( ph -> ( ( ph -> ps ) -> ps ) )
2 1 a1d 
 |-  ( ph -> ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ( ph -> ps ) -> ps ) ) )
3 pm2.21 
 |-  ( -. ph -> ( ph -> ch ) )
4 3 a1d 
 |-  ( -. ph -> ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ph -> ch ) ) )
5 simplim 
 |-  ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ( ph -> ch ) -> ps ) )
6 4 5 sylcom 
 |-  ( -. ph -> ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ps ) )
7 6 a1dd 
 |-  ( -. ph -> ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ( ph -> ps ) -> ps ) ) )
8 2 7 pm2.61i 
 |-  ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ( ph -> ps ) -> ps ) )
9 conax1 
 |-  ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> -. ch )
10 8 9 jcnd 
 |-  ( -. ( ( ( ph -> ch ) -> ps ) -> ch ) -> -. ( ( ( ph -> ps ) -> ps ) -> ch ) )
11 10 con4i 
 |-  ( ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ( ph -> ch ) -> ps ) -> ch ) )
12 conax1 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> -. ch )
13 con3 
 |-  ( ( ph -> ch ) -> ( -. ch -> -. ph ) )
14 12 13 syl5com 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ph -> ch ) -> -. ph ) )
15 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
16 14 15 syl6 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ph -> ch ) -> ( ph -> ps ) ) )
17 pm2.521g2 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ph -> ch ) -> ( ( ph -> ps ) -> ps ) ) )
18 16 17 mpdd 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ph -> ch ) -> ps ) )
19 jcn 
 |-  ( ( ( ph -> ch ) -> ps ) -> ( -. ch -> -. ( ( ( ph -> ch ) -> ps ) -> ch ) ) )
20 19 a1i 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( ( ( ph -> ch ) -> ps ) -> ( -. ch -> -. ( ( ( ph -> ch ) -> ps ) -> ch ) ) ) )
21 18 20 mpd 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> ( -. ch -> -. ( ( ( ph -> ch ) -> ps ) -> ch ) ) )
22 12 21 mpd 
 |-  ( -. ( ( ( ph -> ps ) -> ps ) -> ch ) -> -. ( ( ( ph -> ch ) -> ps ) -> ch ) )
23 22 con4i 
 |-  ( ( ( ( ph -> ch ) -> ps ) -> ch ) -> ( ( ( ph -> ps ) -> ps ) -> ch ) )
24 11 23 impbii 
 |-  ( ( ( ( ph -> ps ) -> ps ) -> ch ) <-> ( ( ( ph -> ch ) -> ps ) -> ch ) )