Theorem jaoi 368

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)

Hypotheses

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

Assertion

Ref	Expression
jaoi	⊢ ((φ ∨ χ) → ψ)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		pm2.53 362	. . 3 ⊢ ((φ ∨ χ) → (¬ φ → χ))
2		jaoi.2	. . 3 ⊢ (χ → ψ)
3	1, 2	syl6 29	. 2 ⊢ ((φ ∨ χ) → (¬ φ → ψ))
4		jaoi.1	. 2 ⊢ (φ → ψ)
5	3, 4	pm2.61d2 152	1 ⊢ ((φ ∨ χ) → ψ)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357

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

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

This theorem is referenced by:  jaod  369  pm1.4  375  jaoa  496  pm1.2  499  orim12i  502  pm1.5  508  pm2.41  556  pm2.42  557  pm2.4  558  pm4.44  560  jaoian  759  pm2.64  764  pm2.82  825  pm3.2ni  827  andi  837  ecase3  907  consensus  925  cad1  1398  19.33  1607  19.33b  1608  dfsb2  2055  mooran1  2258  2eu3  2286  eueq3  3011  sbcor  3090  elun  3220  sspss  3368  sspsstr  3374  ssun  3442  inss  3484  undif3  3515  ifbi  3679  elpr2  3752  pwpw0  3855  sssn  3864  snsssn  3873  pwsnALT  3882  unissint  3950  pwadjoin  4119  preq12b  4127  abexv  4324  nnc0suc  4412  lefinlteq  4463  ltfintri  4466  clos1basesuc  5882  nchoicelem17  6305