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

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
StepHypRef Expression
1 jaod.1 . . . 4 (φ → (ψχ))
21com12 27 . . 3 (ψ → (φχ))
3 jaod.2 . . . 4 (φ → (θχ))
43com12 27 . . 3 (θ → (φχ))
52, 4jaoi 368 . 2 ((ψ θ) → (φχ))
65com12 27 1 (φ → ((ψ θ) → χ))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator