# Metamath Proof Explorer

Description: An implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction. A utility lemma as illustrated in biadanii and elelb . (Contributed by BJ, 4-Mar-2023) (Proof shortened by Wolf Lammen, 8-Mar-2023)

Ref Expression
`|- ( ( ph -> ps ) <-> ( ( ps -> ( ph <-> ch ) ) <-> ( ph <-> ( ps /\ ch ) ) ) )`

### Proof

Step Hyp Ref Expression
1 pm4.71r
` |-  ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )`
2 bicom
` |-  ( ( ph <-> ( ps /\ ph ) ) <-> ( ( ps /\ ph ) <-> ph ) )`
3 bicom
` |-  ( ( ph <-> ( ps /\ ch ) ) <-> ( ( ps /\ ch ) <-> ph ) )`
4 pm5.32
` |-  ( ( ps -> ( ph <-> ch ) ) <-> ( ( ps /\ ph ) <-> ( ps /\ ch ) ) )`
5 3 4 bibi12i
` |-  ( ( ( ph <-> ( ps /\ ch ) ) <-> ( ps -> ( ph <-> ch ) ) ) <-> ( ( ( ps /\ ch ) <-> ph ) <-> ( ( ps /\ ph ) <-> ( ps /\ ch ) ) ) )`
6 bicom
` |-  ( ( ( ps -> ( ph <-> ch ) ) <-> ( ph <-> ( ps /\ ch ) ) ) <-> ( ( ph <-> ( ps /\ ch ) ) <-> ( ps -> ( ph <-> ch ) ) ) )`
7 biluk
` |-  ( ( ( ps /\ ph ) <-> ph ) <-> ( ( ( ps /\ ch ) <-> ph ) <-> ( ( ps /\ ph ) <-> ( ps /\ ch ) ) ) )`
8 5 6 7 3bitr4ri
` |-  ( ( ( ps /\ ph ) <-> ph ) <-> ( ( ps -> ( ph <-> ch ) ) <-> ( ph <-> ( ps /\ ch ) ) ) )`
9 1 2 8 3bitri
` |-  ( ( ph -> ps ) <-> ( ( ps -> ( ph <-> ch ) ) <-> ( ph <-> ( ps /\ ch ) ) ) )`