Theorem jaodan 799

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 115	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 719	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 124	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  800  ordi  818  andi  820  dcor  938  ccase  967  mpjao3dan  1320  relop  4828  poltletr  5083  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  phplem3  6951  ssfilem  6972  diffitest  6984  reapmul1  8668  apsqgt0  8674  recexaplem2  8725  nnnn0addcl  9325  un0addcl  9328  un0mulcl  9329  elz2  9444  xrltso  9918  xaddnemnf  9979  xaddnepnf  9980  fzsplit2  10172  fzsuc2  10201  elfzp12  10221  seqf1oglem2  10665  expp1  10691  expnegap0  10692  expcllem  10695  mulexpzap  10724  expaddzap  10728  expmulzap  10730  zzlesq  10853  bcpasc  10911  ccatass  11064  ccatrn  11065  ccatswrd  11123  xrltmaxsup  11568  xrmaxaddlem  11571  summodc  11694  fsumsplit  11718  fprodsplitdc  11907  ef0lem  11971  odd2np1  12184  dvdslcm  12391  lcmeq0  12393  lcmcl  12394  lcmneg  12396  lcmgcd  12400  rpexp1i  12476  pcid  12647  4sqlem16  12729  xpsfeq  13177  mulgneg  13476  mulgnn0z  13485  lgsdir2lem4  15508  lgsdir2  15510  lgsdirnn0  15524  lgsdinn0  15525