Theorem jaodan 769

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 114	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 114	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 689	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 123	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  770  ordi  788  andi  790  dcor  902  ccase  931  mpjao3dan  1268  relop  4649  poltletr  4897  tfrlemisucaccv  6176  tfr1onlemsucaccv  6192  tfrcllemsucaccv  6205  phplem3  6701  ssfilem  6722  diffitest  6734  reapmul1  8275  apsqgt0  8281  recexaplem2  8326  nnnn0addcl  8911  un0addcl  8914  un0mulcl  8915  elz2  9026  xrltso  9475  xaddnemnf  9533  xaddnepnf  9534  fzsplit2  9723  fzsuc2  9752  elfzp12  9772  expp1  10193  expnegap0  10194  expcllem  10197  mulexpzap  10226  expaddzap  10230  expmulzap  10232  bcpasc  10405  xrltmaxsup  10918  xrmaxaddlem  10921  summodc  11044  fsumsplit  11068  ef0lem  11217  odd2np1  11418  dvdslcm  11596  lcmeq0  11598  lcmcl  11599  lcmneg  11601  lcmgcd  11605  rpexp1i  11678