Metamath Proof Explorer


Theorem 2falsedOLD

Description: Obsolete version of 2falsed as of 11-Apr-2024. (Contributed by NM, 11-Oct-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses 2falsed.1
|- ( ph -> -. ps )
2falsed.2
|- ( ph -> -. ch )
Assertion 2falsedOLD
|- ( ph -> ( ps <-> ch ) )

Proof

Step Hyp Ref Expression
1 2falsed.1
 |-  ( ph -> -. ps )
2 2falsed.2
 |-  ( ph -> -. ch )
3 1 pm2.21d
 |-  ( ph -> ( ps -> ch ) )
4 2 pm2.21d
 |-  ( ph -> ( ch -> ps ) )
5 3 4 impbid
 |-  ( ph -> ( ps <-> ch ) )