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

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-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  341  equsex  1722  equsexd  1723  rexim  2565  rr19.28v  2871  sotricim  4309  sotritrieq  4311  ordsucss  4489  ordpwsucss  4552  peano5  4583  iss  4938  funssres  5242  ssimaex  5561  elpreima  5619  resflem  5664  tposfo2  6250  nnmord  6500  map0g  6670  mapsn  6672  enq0tr  7400  addnqprl  7495  addnqpru  7496  cauappcvgprlemdisj  7617  lttri3  8003  ltleap  8555  mulgt1  8783  nominpos  9119  uzind  9327  indstr  9556  eqreznegel  9577  shftuz  10785  caucvgrelemcau  10948  sqrtsq  11012  mulcn2  11279  dvdsgcdb  11972  algcvgblem  12007  lcmdvdsb  12042  rpexp  12111  infpnlem1  12315  cnntr  13104  cnrest2  13115  txlm  13158  metrest  13385  bj-om  14057