Theorem jaodan 805

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  806  ordi  824  andi  826  dcor  944  ccase  973  mpjao3dan  1344  relop  4910  poltletr  5168  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  phplem3  7121  ssfilem  7143  ssfilemd  7145  diffitest  7157  pr1or2  7504  reapmul1  8886  apsqgt0  8892  recexaplem2  8943  nnnn0addcl  9543  un0addcl  9546  un0mulcl  9547  elz2  9666  xrltso  10148  xaddnemnf  10209  xaddnepnf  10210  fzsplit2  10404  fzsplit3  10407  fzsuc2  10435  elfzp12  10455  seqf1oglem2  10906  expp1  10932  expnegap0  10933  expcllem  10936  mulexpzap  10965  expaddzap  10969  expmulzap  10971  zzlesq  11095  bcpasc  11153  ccatass  11321  ccatrn  11322  ccatswrd  11387  ccatpfx  11418  cats1un  11438  xrltmaxsup  11967  xrmaxaddlem  11970  summodc  12094  fsumsplit  12118  fprodsplitdc  12307  ef0lem  12371  odd2np1  12584  dvdslcm  12791  lcmeq0  12793  lcmcl  12794  lcmneg  12796  lcmgcd  12800  rpexp1i  12876  pcid  13047  4sqlem16  13129  xpsfeq  13609  mulgneg  13893  mulgnn0z  13902  lgsdir2lem4  16030  lgsdir2  16032  lgsdirnn0  16046  lgsdinn0  16047