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  340  equsex  1706  equsexd  1707  rexim  2526  rr19.28v  2824  sotricim  4245  sotritrieq  4247  ordsucss  4420  ordpwsucss  4482  peano5  4512  iss  4865  funssres  5165  ssimaex  5482  elpreima  5539  resflem  5584  tposfo2  6164  nnmord  6413  map0g  6582  mapsn  6584  enq0tr  7242  addnqprl  7337  addnqpru  7338  cauappcvgprlemdisj  7459  lttri3  7844  ltleap  8394  mulgt1  8621  nominpos  8957  uzind  9162  indstr  9388  eqreznegel  9406  shftuz  10589  caucvgrelemcau  10752  sqrtsq  10816  mulcn2  11081  dvdsgcdb  11701  algcvgblem  11730  lcmdvdsb  11765  rpexp  11831  cnntr  12394  cnrest2  12405  txlm  12448  metrest  12675  bj-om  13135