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  4878  poltletr  5135  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  phplem3  7035  ssfilem  7057  diffitest  7069  pr1or2  7390  reapmul1  8765  apsqgt0  8771  recexaplem2  8822  nnnn0addcl  9422  un0addcl  9425  un0mulcl  9426  elz2  9541  xrltso  10021  xaddnemnf  10082  xaddnepnf  10083  fzsplit2  10275  fzsuc2  10304  elfzp12  10324  seqf1oglem2  10772  expp1  10798  expnegap0  10799  expcllem  10802  mulexpzap  10831  expaddzap  10835  expmulzap  10837  zzlesq  10960  bcpasc  11018  ccatass  11175  ccatrn  11176  ccatswrd  11241  ccatpfx  11272  cats1un  11292  xrltmaxsup  11808  xrmaxaddlem  11811  summodc  11934  fsumsplit  11958  fprodsplitdc  12147  ef0lem  12211  odd2np1  12424  dvdslcm  12631  lcmeq0  12633  lcmcl  12634  lcmneg  12636  lcmgcd  12640  rpexp1i  12716  pcid  12887  4sqlem16  12969  xpsfeq  13418  mulgneg  13717  mulgnn0z  13726  lgsdir2lem4  15750  lgsdir2  15752  lgsdirnn0  15766  lgsdinn0  15767