ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jcad Structured version   Unicode 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  6512  addnqpru  6513  lttri3  6855  ltleap  7373  mulgt1  7570  nominpos  7899  uzind  8085  indstr  8272  eqreznegel  8285  bj-om  9325  peano5set  9328
  Copyright terms: Public domain W3C validator