New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  jaoi GIF version

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
StepHypRef Expression
1 pm2.53 362 . . 3 ((φ χ) → (¬ φχ))
2 jaoi.2 . . 3 (χψ)
31, 2syl6 29 . 2 ((φ χ) → (¬ φψ))
4 jaoi.1 . 2 (φψ)
53, 4pm2.61d2 152 1 ((φ χ) → ψ)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator