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  4905  poltletr  5163  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  phplem3  7108  ssfilem  7130  ssfilemd  7132  diffitest  7144  pr1or2  7491  reapmul1  8869  apsqgt0  8875  recexaplem2  8926  nnnn0addcl  9526  un0addcl  9529  un0mulcl  9530  elz2  9649  xrltso  10129  xaddnemnf  10190  xaddnepnf  10191  fzsplit2  10384  fzsuc2  10413  elfzp12  10433  seqf1oglem2  10882  expp1  10908  expnegap0  10909  expcllem  10912  mulexpzap  10941  expaddzap  10945  expmulzap  10947  zzlesq  11070  bcpasc  11128  ccatass  11296  ccatrn  11297  ccatswrd  11362  ccatpfx  11393  cats1un  11413  xrltmaxsup  11942  xrmaxaddlem  11945  summodc  12069  fsumsplit  12093  fprodsplitdc  12282  ef0lem  12346  odd2np1  12559  dvdslcm  12766  lcmeq0  12768  lcmcl  12769  lcmneg  12771  lcmgcd  12775  rpexp1i  12851  pcid  13022  4sqlem16  13104  xpsfeq  13558  mulgneg  13857  mulgnn0z  13866  lgsdir2lem4  15904  lgsdir2  15906  lgsdirnn0  15920  lgsdinn0  15921