Metamath Proof Explorer

Theorem axio

Description: Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 jaob 
 |-  ( ( ( ph \/ ch ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) ) )