Theorem jaob 422

Description: Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121.

Assertion

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

Proof of Theorem jaob

Step	Hyp	Ref	Expression
1		orc 269	. . . 4 |- (ph -> (ph \/ ch))
2	1	imim1i 16	. . 3 |- (((ph \/ ch) -> ps) -> (ph -> ps))
3		olc 268	. . . 4 |- (ch -> (ph \/ ch))
4	3	imim1i 16	. . 3 |- (((ph \/ ch) -> ps) -> (ch -> ps))
5	2, 4	jca 288	. 2 |- (((ph \/ ch) -> ps) -> ((ph -> ps) /\ (ch -> ps)))
6		jao 340	. . 3 |- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
7	6	imp 350	. 2 |- (((ph -> ps) /\ (ch -> ps)) -> ((ph \/ ch) -> ps))
8	5, 7	impbi 157	1 |- (((ph \/ ch) -> ps) <-> ((ph -> ps) /\ (ch -> ps)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223

This theorem is referenced by:  pm4.77 423  pm3.44 430  pm5.53 483  pm4.83 739  unss 2201  ralpr 2425  prsspw 2477  intun 2558  intpr 2559  ordsseleq 2972  relop 3271  cau2 6865  caubnd 6878  spwpr2 8615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain