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

Theorem jcad 291
Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
jcad.1 (φ → (ψχ))
jcad.2 (φ → (ψθ))
Assertion
Ref Expression
jcad (φ → (ψ → (χ θ)))

Proof of Theorem jcad
StepHypRef Expression
1 jcad.1 . 2 (φ → (ψχ))
2 jcad.2 . 2 (φ → (ψθ))
3 pm3.2 126 . 2 (χ → (θ → (χ θ)))
41, 2, 3syl6c 60 1 (φ → (ψ → (χ θ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  jctild  299  jctird  300  ancld  308  ancrd  309  anim12ii  325  equsex  1598  equsexd  1599  rexim  2391  rr19.28v  2660  sotricim  4034  sotritrieq  4036  ordsucss  4180  ordpwsucss  4227  peano5  4248  iss  4581  funssres  4868  ssimaex  5159  elpreima  5211  tposfo2  5804  nnmord  6001  enq0tr  6289  addnqprl  6384  addnqpru  6385  bj-om  7306  peano5set  7309
  Copyright terms: Public domain W3C validator