Theorem jaodan 809

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4930  poltletr  5188  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  phplem3  7155  ssfilem  7177  ssfilemd  7179  diffitest  7191  pr1or2  7540  reapmul1  8925  apsqgt0  8931  recexaplem2  8982  nnnn0addcl  9597  un0addcl  9600  un0mulcl  9601  elz2  9720  xrltso  10208  xaddnemnf  10269  xaddnepnf  10270  fzsplit2  10465  fzsplit3  10468  fzsuc2  10496  elfzp12  10516  seqf1oglem2  10970  expp1  10996  expnegap0  10997  expcllem  11000  mulexpzap  11029  expaddzap  11033  expmulzap  11035  zzlesq  11159  bcpasc  11218  ccatass  11390  ccatrn  11391  ccatswrd  11456  ccatpfx  11487  cats1un  11507  xrltmaxsup  12039  xrmaxaddlem  12042  summodc  12166  fsumsplit  12190  fprodsplitdc  12379  ef0lem  12443  odd2np1  12656  dvdslcm  12863  lcmeq0  12865  lcmcl  12866  lcmneg  12868  lcmgcd  12872  rpexp1i  12949  pcid  13123  4sqlem16  13205  xpsfeq  13715  mulgneg  13992  mulgnn0z  14001  bposlem2  16210  lgsdir2lem4  16248  lgsdir2  16250  lgsdirnn0  16264  lgsdinn0  16265