Theorem jaodan 798

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  799  ordi  817  andi  819  dcor  937  ccase  966  mpjao3dan  1318  relop  4817  poltletr  5071  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  phplem3  6924  ssfilem  6945  diffitest  6957  reapmul1  8639  apsqgt0  8645  recexaplem2  8696  nnnn0addcl  9296  un0addcl  9299  un0mulcl  9300  elz2  9414  xrltso  9888  xaddnemnf  9949  xaddnepnf  9950  fzsplit2  10142  fzsuc2  10171  elfzp12  10191  seqf1oglem2  10629  expp1  10655  expnegap0  10656  expcllem  10659  mulexpzap  10688  expaddzap  10692  expmulzap  10694  zzlesq  10817  bcpasc  10875  xrltmaxsup  11439  xrmaxaddlem  11442  summodc  11565  fsumsplit  11589  fprodsplitdc  11778  ef0lem  11842  odd2np1  12055  dvdslcm  12262  lcmeq0  12264  lcmcl  12265  lcmneg  12267  lcmgcd  12271  rpexp1i  12347  pcid  12518  4sqlem16  12600  xpsfeq  13047  mulgneg  13346  mulgnn0z  13355  lgsdir2lem4  15356  lgsdir2  15358  lgsdirnn0  15372  lgsdinn0  15373