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  1774  equsexd  1775  rexim  2624  rr19.28v  2943  sotricim  4411  sotritrieq  4413  ordsucss  4593  ordpwsucss  4656  peano5  4687  iss  5047  funssres  5356  ssimaex  5688  elpreima  5747  resflem  5792  tposfo2  6403  nnmord  6653  map0g  6825  mapsn  6827  enq0tr  7609  addnqprl  7704  addnqpru  7705  cauappcvgprlemdisj  7826  lttri3  8214  ltleap  8767  mulgt1  8998  nominpos  9337  uzind  9546  indstr  9776  eqreznegel  9797  ccatopth  11234  shftuz  11314  caucvgrelemcau  11477  sqrtsq  11541  mulcn2  11809  dvdsgcdb  12520  algcvgblem  12557  lcmdvdsb  12592  rpexp  12661  infpnlem1  12868  imasring  14013  unitmulclb  14063  cnntr  14884  cnrest2  14895  txlm  14938  metrest  15165  bj-om  16230