ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jcad GIF 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 (𝜑 → (𝜓𝜒))
jcad.2 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
jcad (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem jcad
StepHypRef Expression
1 jcad.1 . 2 (𝜑 → (𝜓𝜒))
2 jcad.2 . 2 (𝜑 → (𝜓𝜃))
3 pm3.2 138 . 2 (𝜒 → (𝜃 → (𝜒𝜃)))
41, 2, 3syl6c 66 1 (𝜑 → (𝜓 → (𝜒𝜃)))
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  1691  equsexd  1692  rexim  2503  rr19.28v  2798  sotricim  4215  sotritrieq  4217  ordsucss  4390  ordpwsucss  4452  peano5  4482  iss  4835  funssres  5135  ssimaex  5450  elpreima  5507  resflem  5552  tposfo2  6132  nnmord  6381  map0g  6550  mapsn  6552  enq0tr  7210  addnqprl  7305  addnqpru  7306  cauappcvgprlemdisj  7427  lttri3  7812  ltleap  8362  mulgt1  8589  nominpos  8925  uzind  9130  indstr  9356  eqreznegel  9374  shftuz  10557  caucvgrelemcau  10720  sqrtsq  10784  mulcn2  11049  dvdsgcdb  11628  algcvgblem  11657  lcmdvdsb  11692  rpexp  11758  cnntr  12321  cnrest2  12332  txlm  12375  metrest  12602  bj-om  13062
  Copyright terms: Public domain W3C validator