ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaod Structured version   GIF version

Theorem jaod 624
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
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 623 . 2 ((ψ θ) → (φχ))
65com12 27 1 (φ → ((ψ θ) → χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpjaod  625  jaao  626  orel2  632  pm2.621  653  mtord  684  jaodan  697  pm2.63  700  pm2.74  707  dedlema  864  dedlemb  865  oplem1  870  opthpr  3517  trsucss  4110  ordsucim  4176  onsucelsucr  4183  0elnn  4267  xpsspw  4377  relop  4413  fununi  4893  poxp  5775  nntri1  5989  nnmordi  6000  nnaordex  6011  nnm00  6013  swoord2  6047  elni2  6174  prubl  6340  distrlem4prl  6423  distrlem4pru  6424  ltxrlt  6686  bj-nntrans  7173  bj-nnelirr  7175  bj-findis  7197
  Copyright terms: Public domain W3C validator