Theorem jaodan 809

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 729	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 124	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4932  poltletr  5191  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  phplem3  7159  ssfilem  7181  ssfilemd  7183  diffitest  7195  pr1or2  7546  reapmul1  8931  apsqgt0  8937  recexaplem2  8988  nnnn0addcl  9604  un0addcl  9607  un0mulcl  9608  elz2  9727  xrltso  10215  xaddnemnf  10276  xaddnepnf  10277  fzsplit2  10472  fzsplit3  10475  fzsuc2  10503  elfzp12  10523  seqf1oglem2  10978  expp1  11004  expnegap0  11005  expcllem  11008  mulexpzap  11037  expaddzap  11041  expmulzap  11043  zzlesq  11167  bcpasc  11226  ccatass  11398  ccatrn  11399  ccatswrd  11464  ccatpfx  11495  cats1un  11515  xrltmaxsup  12048  xrmaxaddlem  12051  summodc  12175  fsumsplit  12199  fprodsplitdc  12388  ef0lem  12452  odd2np1  12665  dvdslcm  12872  lcmeq0  12874  lcmcl  12875  lcmneg  12877  lcmgcd  12881  rpexp1i  12958  pcid  13132  4sqlem16  13214  xpsfeq  13725  mulgneg  14002  mulgnn0z  14011  gsumunsnfd  14259  bposlem2  16312  lgsdir2lem4  16355  lgsdir2  16357  lgsdirnn0  16371  lgsdinn0  16372  idjudju  17252