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

Theorem orim12d 699
Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
orim12d.1 (φ → (ψχ))
orim12d.2 (φ → (θτ))
Assertion
Ref Expression
orim12d (φ → ((ψ θ) → (χ τ)))

Proof of Theorem orim12d
StepHypRef Expression
1 orim12d.1 . 2 (φ → (ψχ))
2 orim12d.2 . 2 (φ → (θτ))
3 pm3.48 698 . 2 (((ψχ) (θτ)) → ((ψ θ) → (χ τ)))
41, 2, 3syl2anc 391 1 (φ → ((ψ θ) → (χ τ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  orim1d  700  orim2d  701  3orim123d  1214  19.33b2  1517  preq12b  3532  prel12  3533  funun  4887  nnsucelsuc  6009  nnaord  6018  nnmord  6026  swoer  6070  ltsopr  6570  cauappcvgprlemloc  6624  caucvgprlemloc  6646  mulextsr1lem  6706  reapcotr  7382  apcotr  7391  mulext1  7396  mulext  7398  peano2z  8057  zeo  8119  uzm1  8279  eluzdc  8323  fzospliti  8802  frec2uzltd  8870  bj-findis  9439
  Copyright terms: Public domain W3C validator