Theorem jcad 455

Description: Deduction conjoining the consequents of two implications.

Hypotheses

Ref	Expression
jcad.1	|- (ph -> (ps -> ch))
jcad.2	|- (ph -> (ps -> th))

Assertion

Ref	Expression
jcad	|- (ph -> (ps -> (ch /\ th)))

Proof of Theorem jcad

Step	Hyp	Ref	Expression
1		jcad.1	. . . 4 |- (ph -> (ps -> ch))
2	1	imp 277	. . 3 |- ((ph /\ ps) -> ch)
3		jcad.2	. . . 4 |- (ph -> (ps -> th))
4	3	imp 277	. . 3 |- ((ph /\ ps) -> th)
5	2, 4	jca 236	. 2 |- ((ph /\ ps) -> (ch /\ th))
6	5	exp 291	1 |- (ph -> (ps -> (ch /\ th)))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  oplem1 578  2eu1 1067  dfwe2 2187  ordunidif 2260  oneqmini 2272  oneqmin 2273  orduniorsuc 2337  funss 2682  funssres 2698  funcnvuni 2706  fnun 2730  fnex 2740  cleqfv 2880  cbvfo 2923  isomin 2937  isofrlem 2939  abianfp 3000  oaordex 3160  oa00 3161  nnarcl 3174  nnaordex 3191  nnawordex 3192  eceqopreq 3249  mapsn 3269  sbthbg 3360  sdomdomtr 3370  ssenen 3399  onomeneq 3414  pssnn 3428  unblem1 3431  unfilem1 3438  fiint 3445  inf0 3457  inf3lem3 3466  inf3lem4 3467  cplem1 3545  karden 3551  aceq5lem5 3562  aceq6b 3565  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodomb 3615  carden 3638  sucdom 3648  cardmin 3666  alephordi 3679  cardinfima 3696  cflim 3704  cfsuc 3709  indpi 3828  genpcl 3905  addclprlem2 3913  ltaddpr 3934  ltexprlem5 3940  suplem1pr 3955  suppsr2 4017  ltlent 4288  add20 4329  ledivt 4405  nominpos 4509  sup2 4510  zaddclt 4590  zmulclt 4596  qnegclt 4643  qbtwnre 4650  infxpidmlem8 4940  infxpidmlem10 4942  ococss 5174  chocuni 5179  occllem6 5185  shlej1t 5356  orthin 5371  spansncol 5473  osumlem4 5533  stm1add 5686  stm1add3 5688  mdbr2 5728  dmdbr2 5733  atcveq0 5746  chrelat2 5758  atexch 5769  atcvat4 5775  mdsymlem3 5778

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org