Theorem jaod 369

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	⊢ (φ → (ψ → χ))
jaod.2	⊢ (φ → (θ → χ))

Assertion

Ref	Expression
jaod	⊢ (φ → ((ψ ∨ θ) → χ))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (φ → (ψ → χ))
2	1	com12 27	. . 3 ⊢ (ψ → (φ → χ))
3		jaod.2	. . . 4 ⊢ (φ → (θ → χ))
4	3	com12 27	. . 3 ⊢ (θ → (φ → χ))
5	2, 4	jaoi 368	. 2 ⊢ ((ψ ∨ θ) → (φ → χ))
6	5	com12 27	1 ⊢ (φ → ((ψ ∨ θ) → χ))

Syntax hints:   → wi 4   ∨ wo 357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359

This theorem is referenced by:  mpjaod  370  orel2  372  pm2.621  397  jaao  495  jaodan  760  pm2.63  763  ecase2d  906  ecase3d  909  dedlema  920  dedlemb  921  cad0  1400  psssstr  3375  opkth1g  4130  lenltfin  4469  ssfin  4470  evenodddisj  4516  vfinspss  4551  vinf  4555  fununi  5160  weds  5938  enprmaplem3  6078  leconnnc  6218  addceq0  6219  nclenn  6249  muc0or  6252  ncslesuc  6267  nnc3n3p1  6278  nchoicelem6  6294  dmfrec  6316  fnfreclem2  6318