Theorem jaodan 426

Description: Deduction disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaodan.1	|- ((ph /\ ps) -> ch)
jaodan.2	|- ((ph /\ th) -> ch)

Assertion

Ref	Expression
jaodan	|- ((ph /\ (ps \/ th)) -> ch)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 373	. . 3 |- (ph -> (ps -> ch))
3		jaodan.2	. . . 4 |- ((ph /\ th) -> ch)
4	3	ex 373	. . 3 |- (ph -> (th -> ch))
5	2, 4	jaod 424	. 2 |- (ph -> ((ps \/ th) -> ch))
6	5	imp 350	1 |- ((ph /\ (ps \/ th)) -> ch)

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

This theorem is referenced by:  opth1gOLD 2788  relop 3265  phplem3 4490  ssnn 4514  1re 5407  lecase 5595  recextlem2 5656  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  flhalft 6189  expcllem 6507  expge1t 6524  exple1t 6538  cvg3 6860  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd4 6889  fsumcmpndx2 6980  elcncf 7200  reeff1o 7368  ssblex 7796  lmsslem 7887  bcthlem16 7948  bcthlem20 7952  hmopidmchlem 9989

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