Theorem jaodan 710

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

Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mpjaodan  711  ordi  729  andi  731  dcor  843  ccase  871  mpjao3dan  1202  relop  4486  poltletr  4725  tfrlemisucaccv  5939  phplem3  6317  ssfiexmid  6336  diffitest  6344  reapmul1  7584  apsqgt0  7590  recexaplem2  7631  nnnn0addcl  8210  un0addcl  8213  un0mulcl  8214  elz2  8310  xrltso  8715  fzsplit2  8912  fzsuc2  8939  elfzp12  8959  expp1  9236  expnegap0  9237  expcllem  9240  mulexpzap  9269  expaddzap  9273  expmulzap  9275