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

Theorem jcad 305
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 138 . 2  |-  ( ch 
->  ( th  ->  ( ch  /\  th ) ) )
41, 2, 3syl6c 66 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  jca2  306  jctild  314  jctird  315  ancld  323  ancrd  324  anim12ii  340  equsex  1706  equsexd  1707  rexim  2526  rr19.28v  2824  sotricim  4245  sotritrieq  4247  ordsucss  4420  ordpwsucss  4482  peano5  4512  iss  4865  funssres  5165  ssimaex  5482  elpreima  5539  resflem  5584  tposfo2  6164  nnmord  6413  map0g  6582  mapsn  6584  enq0tr  7249  addnqprl  7344  addnqpru  7345  cauappcvgprlemdisj  7466  lttri3  7851  ltleap  8401  mulgt1  8628  nominpos  8964  uzind  9169  indstr  9395  eqreznegel  9413  shftuz  10596  caucvgrelemcau  10759  sqrtsq  10823  mulcn2  11088  dvdsgcdb  11707  algcvgblem  11736  lcmdvdsb  11771  rpexp  11837  cnntr  12403  cnrest2  12414  txlm  12457  metrest  12684  bj-om  13188
  Copyright terms: Public domain W3C validator