Metamath Proof Explorer

Theorem imadisjld

Description: Natural dduction form of one side of imadisj . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypothesis imadisjld.1 
|- ( ph -> ( dom A i^i B ) = (/) )
Assertion imadisjld 
|- ( ph -> ( A " B ) = (/) )

Proof

Step Hyp Ref Expression
1 imadisjld.1 
 |-  ( ph -> ( dom A i^i B ) = (/) )
2 imadisj 
 |-  ( ( A " B ) = (/) <-> ( dom A i^i B ) = (/) )
3 1 2 sylibr 
 |-  ( ph -> ( A " B ) = (/) )