Theorem jaodan 802

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  803  ordi  821  andi  823  dcor  941  ccase  970  mpjao3dan  1341  relop  4871  poltletr  5128  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  phplem3  7011  ssfilem  7033  diffitest  7045  pr1or2  7363  reapmul1  8738  apsqgt0  8744  recexaplem2  8795  nnnn0addcl  9395  un0addcl  9398  un0mulcl  9399  elz2  9514  xrltso  9988  xaddnemnf  10049  xaddnepnf  10050  fzsplit2  10242  fzsuc2  10271  elfzp12  10291  seqf1oglem2  10737  expp1  10763  expnegap0  10764  expcllem  10767  mulexpzap  10796  expaddzap  10800  expmulzap  10802  zzlesq  10925  bcpasc  10983  ccatass  11138  ccatrn  11139  ccatswrd  11197  ccatpfx  11228  cats1un  11248  xrltmaxsup  11763  xrmaxaddlem  11766  summodc  11889  fsumsplit  11913  fprodsplitdc  12102  ef0lem  12166  odd2np1  12379  dvdslcm  12586  lcmeq0  12588  lcmcl  12589  lcmneg  12591  lcmgcd  12595  rpexp1i  12671  pcid  12842  4sqlem16  12924  xpsfeq  13373  mulgneg  13672  mulgnn0z  13681  lgsdir2lem4  15704  lgsdir2  15706  lgsdirnn0  15720  lgsdinn0  15721