Theorem jca 236

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'").

Hypotheses

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

Assertion

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

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. . 3 |- (ph -> ps)
2		jca.2	. . 3 |- (ph -> ch)
3	1, 2	jc 119	. 2 |- (ph -> -. (ps -> -. ch))
4		df-an 198	. 2 |- ((ps /\ ch) <-> -. (ps -> -. ch))
5	3, 4	sylibr 175	1 |- (ph -> (ps /\ ch))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196

This theorem is referenced by:  jcai 237  jctl 238  jctr 239  jctil 240  jctir 241  ancli 244  ancri 245  anim12i 268  jaob 328  ancom 333  abai 366  anabs1 374  anabs7 376  impbid 397  ordi 452  jcad 455  pm5.18 497  ecase2d 558  3jca 604  ecased 643  19.26 749  19.40 773  a4c1 844  sb2 859  sbequ1 863  sbn2 881  eu2 1023  mooran2 1050  2eu1 1067  2eu3 1069  r19.40 1301  eqssd 1518  psstr 1574  ssin 1659  unineq 1680  un00 1728  raaan 1775  prss 1854  prel12 1875  opthwiener 1914  unexb 1950  opeluu 1953  euuni 1954  itlso 2151  supmo 2156  supsn 2168  wereu 2197  elon2 2210  ordelord 2221  tz7.7 2224  suceloni 2314  ordnbtwn 2316  dflim3 2368  ordom 2382  omssnlim 2386  opthprc 2457  xpex 2488  dminss 2648  imainss 2649  relssdr 2668  cnvexg 2669  dffun7 2688  funun 2700  fununi 2705  fun11uni 2707  resfunexg 2717  fnssres 2734  fnopabg 2745  fss 2759  fco 2760  f00 2773  fconstg 2775  f1o2 2804  f1f1orn 2810  f1ocnv 2811  f1oco 2816  f1o00 2823  fv3 2839  fvelrn 2883  fopab2 2891  ffnfv 2892  fsn2 2896  fconstfv 2903  f1ocnvfv1 2919  f1ocnvfv2 2920  isocnv 2934  isotr 2935  isotrALT 2936  f1oiso 2942  tfrlem8 2956  tfrlem10 2958  tfrlem12 2960  oalim 3135  omlim 3136  oelim 3137  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  omsmo 3196  map0 3268  bren2 3293  en2d 3303  dom2d 3307  sdomex 3315  2dom 3332  xpdom2 3345  sbthlem9 3357  mapenlem2 3385  mapxpen 3390  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395  mapunen 3397  php2 3410  php3 3411  onomeneq 3414  omsdomnn 3424  unblem1 3431  unblem4 3434  unfilem1 3438  inf5 3472  infensuc 3484  r1ord 3499  r1val1 3502  rankr1 3518  aceq3 3556  ac6lem 3575  fodom 3613  fodomb 3615  sucxpdom 3652  cardsdomel 3658  ondomon 3662  ondomcard 3663  carduni 3664  cardmin 3666  ltsopi 3810  addclpi 3814  mulclpi 3815  addcmpblnq 3846  addclpq 3852  addasspq 3857  distrpqlem 3860  distrpq 3861  1qec 3862  ltsopq 3869  ltexpq 3874  ltbtwnpq 3878  genpcl 3905  1pr 3911  prlem934 3933  ltexprlem5 3940  reclem2pr 3951  reclem3pr 3952  suppr 3957  mulclsr 3987  mulasssr 3993  distrsr 3994  ltsosr 3997  recexsrlem 4006  suppsrlem 4015  suprelem 4053  axmulass 4073  axdistr 4074  axrecex 4079  divmuldivt 4263  divadddivt 4264  divdivdivt 4265  divdiv23t 4271  ltso 4279  nnleltp1t 4448  nnaddm1clt 4452  nnreclt 4522  cru 4529  nn0ltp1let 4556  nnnegz 4566  elnnz 4572  elnnz1 4581  elnn0nn 4593  zltp1let 4597  sqznn 4600  peano2uz 4602  uzind 4603  uzwo2 4606  btwnz 4613  uzwo3lem1 4614  flidt 4627  qret 4631  qaddclt 4642  qnegclt 4643  qrecclt 4646  qbtwnre 4650  seqrn2 4674  nn0opth 4724  sqr2irrlem1 4777  replimt 4798  abs00 4839  abslt 4855  absle 4856  climunii 4883  ruclem4 4888  znnen 4930  infxpidmlem7 4939  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infmap2lem2 4952  infmap2 4953  normpyct 5093  bcs 5101  hlimunii 5143  ocsh 5164  ocin 5177  occllem6 5185  occl 5188  projlem10 5202  projlem25 5217  projlem26 5218  projlem29 5221  pjthlem10 5234  pjthu 5241  pjthu2 5242  dfch2 5254  pjpjtht 5262  pjoml 5271  shscl 5282  ococint 5298  shlub 5347  shslub 5359  chj00 5408  spansnmul 5469  spanunsn 5482  osumlem3 5532  5oalem1 5544  5oalem2 5545  5oalem4 5547  5oalem5 5548  3oalem2 5553  pjorth 5559  pjssm 5572  pjjs 5585  pjin2 5647  pjclem4 5653  pj3s 5659  stles 5682  stadd3 5689  strlem3a 5693  strlem6 5697  golem1 5704  h1dat 5747  atom1d 5750  atcvatlem 5770  atcvat3 5774  atcvat4 5775  mdsymlem2 5777  mdsymlem5 5780  mdsym 5784  sumdmdi 5785

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