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  1613  equsexd  1614  rexim  2407  rr19.28v  2677  sotricim  4051  sotritrieq  4053  ordsucss  4196  ordpwsucss  4243  peano5  4264  iss  4597  funssres  4885  ssimaex  5177  elpreima  5229  tposfo2  5823  nnmord  6026  enq0tr  6416  addnqprl  6511  addnqpru  6512  cauappcvgprlemdisj  6622  lttri3  6875  ltleap  7393  mulgt1  7590  nominpos  7919  uzind  8105  indstr  8292  eqreznegel  8305  sqrtsq  9194  bj-om  9371  peano5set  9374
  Copyright terms: Public domain W3C validator