Theorem jcad 307

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 139	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 66	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  jca2  308  jctild  316  jctird  317  ancld  325  ancrd  326  anim12ii  343  equsex  1728  equsexd  1729  rexim  2571  rr19.28v  2877  sotricim  4322  sotritrieq  4324  ordsucss  4502  ordpwsucss  4565  peano5  4596  iss  4952  funssres  5257  ssimaex  5576  elpreima  5634  resflem  5679  tposfo2  6265  nnmord  6515  map0g  6685  mapsn  6687  enq0tr  7430  addnqprl  7525  addnqpru  7526  cauappcvgprlemdisj  7647  lttri3  8033  ltleap  8585  mulgt1  8816  nominpos  9152  uzind  9360  indstr  9589  eqreznegel  9610  shftuz  10819  caucvgrelemcau  10982  sqrtsq  11046  mulcn2  11313  dvdsgcdb  12006  algcvgblem  12041  lcmdvdsb  12076  rpexp  12145  infpnlem1  12349  unitmulclb  13214  cnntr  13596  cnrest2  13607  txlm  13650  metrest  13877  bj-om  14549