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

Theorem jcad 295
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 130 . 2 (𝜒 → (𝜃 → (𝜒𝜃)))
41, 2, 3syl6c 64 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  jctild  303  jctird  304  ancld  312  ancrd  313  anim12ii  329  equsex  1632  equsexd  1633  rexim  2430  rr19.28v  2706  sotricim  4088  sotritrieq  4090  ordsucss  4258  ordpwsucss  4319  peano5  4349  iss  4682  funssres  4970  ssimaex  5262  elpreima  5314  tposfo2  5913  nnmord  6121  enq0tr  6590  addnqprl  6685  addnqpru  6686  cauappcvgprlemdisj  6807  lttri3  7157  ltleap  7695  mulgt1  7904  nominpos  8219  uzind  8408  indstr  8632  eqreznegel  8646  shftuz  9646  caucvgrelemcau  9807  sqrtsq  9871  mulcn2  10064  algcvgblem  10271  bj-om  10448  peano5setOLD  10452
  Copyright terms: Public domain W3C validator