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-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:  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  3012  sbcor  3091  elun  3221  sspss  3369  sspsstr  3375  ssun  3443  inss  3485  undif3  3516  ifbi  3680  elpr2  3753  pwpw0  3856  sssn  3865  snsssn  3874  pwsnALT  3883  unissint  3951  pwadjoin  4120  preq12b  4128  abexv  4325  nnc0suc  4413  lefinlteq  4464  ltfintri  4467  clos1basesuc  5883  nchoicelem17  6306