NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  jcad Unicode version

Theorem jcad 519
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 434 . 2
41, 2, 3syl6c 60 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  jctild  527  jctird  528  ancld  536  ancrd  537  anim12ii  553  oplem1  930  rr19.28v  2981  tfinltfinlem1  4500  iss  5000  funssres  5144  elpreima  5407  mapsn  6026  enadjlem1  6059  leltctr  6212  nchoicelem8  6296
  Copyright terms: Public domain W3C validator