Theorem jaob 424

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 425  pm3.44 432  pm5.53 485  pm4.83 742  unss 2207  ralpr 2432  prsspw 2484  intun 2566  intpr 2567  ordsseleq 2982  relop 3281  cau2 6913  caubnd 6926  spwpr2 8654

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