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

Theorem jcad 303
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-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  jca2  304  jctild  312  jctird  313  ancld  321  ancrd  322  anim12ii  338  equsex  1674  equsexd  1675  rexim  2485  rr19.28v  2778  sotricim  4183  sotritrieq  4185  ordsucss  4358  ordpwsucss  4420  peano5  4450  iss  4801  funssres  5101  ssimaex  5414  elpreima  5471  resflem  5516  tposfo2  6094  nnmord  6343  map0g  6512  mapsn  6514  enq0tr  7143  addnqprl  7238  addnqpru  7239  cauappcvgprlemdisj  7360  lttri3  7715  ltleap  8259  mulgt1  8479  nominpos  8809  uzind  9014  indstr  9238  eqreznegel  9256  shftuz  10430  caucvgrelemcau  10592  sqrtsq  10656  mulcn2  10920  dvdsgcdb  11494  algcvgblem  11523  lcmdvdsb  11558  rpexp  11624  cnntr  12175  cnrest2  12186  txlm  12229  metrest  12434  bj-om  12720
  Copyright terms: Public domain W3C validator