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

Theorem jcad 301
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  |-  ( ph  ->  ( ps  ->  ch ) )
jcad.2  |-  ( ph  ->  ( ps  ->  th )
)
Assertion
Ref Expression
jcad  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )

Proof of Theorem jcad
StepHypRef Expression
1 jcad.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 jcad.2 . 2  |-  ( ph  ->  ( ps  ->  th )
)
3 pm3.2 137 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 65 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  jctild  309  jctird  310  ancld  318  ancrd  319  anim12ii  335  equsex  1657  equsexd  1658  rexim  2456  rr19.28v  2735  sotricim  4086  sotritrieq  4088  ordsucss  4256  ordpwsucss  4318  peano5  4347  iss  4684  funssres  4972  ssimaex  5266  elpreima  5318  tposfo2  5916  nnmord  6156  enq0tr  6686  addnqprl  6781  addnqpru  6782  cauappcvgprlemdisj  6903  lttri3  7258  ltleap  7797  mulgt1  8008  nominpos  8335  uzind  8539  indstr  8762  eqreznegel  8780  shftuz  9843  caucvgrelemcau  10004  sqrtsq  10068  mulcn2  10289  dvdsgcdb  10546  algcvgblem  10575  lcmdvdsb  10610  rpexp  10676  bj-om  10917
  Copyright terms: Public domain W3C validator