Theorem jcad 302

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

Step	Hyp	Ref	Expression
1		jcad.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jcad.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		pm3.2 138	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 66	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

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:  jctild  310  jctird  311  ancld  319  ancrd  320  anim12ii  336  equsex  1664  equsexd  1665  rexim  2468  rr19.28v  2757  sotricim  4159  sotritrieq  4161  ordsucss  4334  ordpwsucss  4396  peano5  4426  iss  4771  funssres  5069  ssimaex  5378  elpreima  5432  resflem  5476  tposfo2  6046  nnmord  6290  map0g  6459  mapsn  6461  enq0tr  7047  addnqprl  7142  addnqpru  7143  cauappcvgprlemdisj  7264  lttri3  7619  ltleap  8161  mulgt1  8378  nominpos  8707  uzind  8911  indstr  9135  eqreznegel  9153  shftuz  10305  caucvgrelemcau  10467  sqrtsq  10531  mulcn2  10755  dvdsgcdb  11334  algcvgblem  11363  lcmdvdsb  11398  rpexp  11464  bj-om  12098