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  11294  ccatrn  11295  ccatswrd  11360  ccatpfx  11391  cats1un  11411  xrltmaxsup  11940  xrmaxaddlem  11943  summodc  12067  fsumsplit  12091  fprodsplitdc  12280  ef0lem  12344  odd2np1  12557  dvdslcm  12764  lcmeq0  12766  lcmcl  12767  lcmneg  12769  lcmgcd  12773  rpexp1i  12849  pcid  13020  4sqlem16  13102  xpsfeq  13556  mulgneg  13855  mulgnn0z  13864  lgsdir2lem4  15902  lgsdir2  15904  lgsdirnn0  15918  lgsdinn0  15919