ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orim12d Structured version   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  6568  mulextsr1lem  6666  reapcotr  7342  apcotr  7351  mulext1  7356  mulext  7358  peano2z  8017  zeo  8079  uzm1  8239  eluzdc  8283  fzospliti  8762  frec2uzltd  8830  bj-findis  9363
  Copyright terms: Public domain W3C validator