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  4846  poltletr  5102  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  phplem3  6976  ssfilem  6998  diffitest  7010  pr1or2  7328  reapmul1  8703  apsqgt0  8709  recexaplem2  8760  nnnn0addcl  9360  un0addcl  9363  un0mulcl  9364  elz2  9479  xrltso  9953  xaddnemnf  10014  xaddnepnf  10015  fzsplit2  10207  fzsuc2  10236  elfzp12  10256  seqf1oglem2  10702  expp1  10728  expnegap0  10729  expcllem  10732  mulexpzap  10761  expaddzap  10765  expmulzap  10767  zzlesq  10890  bcpasc  10948  ccatass  11102  ccatrn  11103  ccatswrd  11161  ccatpfx  11192  cats1un  11212  xrltmaxsup  11683  xrmaxaddlem  11686  summodc  11809  fsumsplit  11833  fprodsplitdc  12022  ef0lem  12086  odd2np1  12299  dvdslcm  12506  lcmeq0  12508  lcmcl  12509  lcmneg  12511  lcmgcd  12515  rpexp1i  12591  pcid  12762  4sqlem16  12844  xpsfeq  13292  mulgneg  13591  mulgnn0z  13600  lgsdir2lem4  15623  lgsdir2  15625  lgsdirnn0  15639  lgsdinn0  15640