ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jcad GIF 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 (𝜑 → (𝜓𝜒))
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  304  jctild  312  jctird  313  ancld  321  ancrd  322  anim12ii  338  equsex  1689  equsexd  1690  rexim  2501  rr19.28v  2796  sotricim  4213  sotritrieq  4215  ordsucss  4388  ordpwsucss  4450  peano5  4480  iss  4833  funssres  5133  ssimaex  5448  elpreima  5505  resflem  5550  tposfo2  6130  nnmord  6379  map0g  6548  mapsn  6550  enq0tr  7206  addnqprl  7301  addnqpru  7302  cauappcvgprlemdisj  7423  lttri3  7808  ltleap  8357  mulgt1  8581  nominpos  8911  uzind  9116  indstr  9340  eqreznegel  9358  shftuz  10540  caucvgrelemcau  10703  sqrtsq  10767  mulcn2  11032  dvdsgcdb  11608  algcvgblem  11637  lcmdvdsb  11672  rpexp  11738  cnntr  12300  cnrest2  12311  txlm  12354  metrest  12581  bj-om  12969
  Copyright terms: Public domain W3C validator