Theorem jca 518

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Equivalent to the natural deduction rule /\ I (/\ introduction), see natded in set.mm. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

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	. 2 |- (ph -> ps)
2		jca.2	. 2 |- (ph -> ch)
3		pm3.2 434	. 2 |- (ps -> (ch -> (ps /\ ch)))
4	1, 2, 3	sylc 56	1 |- (ph -> (ps /\ ch))

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  jca31  520  jca32  521  jcai  522  jctil  523  jctir  524  ancli  534  ancri  535  sylanbrc  645  jaob  758  jcab  833  mpbi2and  887  mpbir2and  888  pm4.82  894  rnlem  931  syl22anc  1183  syl112anc  1186  syl121anc  1187  syl211anc  1188  syl23anc  1189  syl32anc  1190  syl122anc  1191  syl212anc  1192  syl221anc  1193  syl222anc  1198  syl123anc  1199  syl132anc  1200  syl213anc  1201  syl231anc  1202  syl312anc  1203  syl321anc  1204  syl223anc  1208  syl232anc  1209  syl322anc  1210  syl233anc  1211  syl323anc  1212  syl332anc  1213  19.26  1593  19.40  1609  ax12olem3  1929  eu2  2229  mooran2  2259  2eu1  2284  2eu3  2286  2eu6  2289  datisi  2313  felapton  2317  darapti  2318  dimatis  2320  fresison  2321  fesapo  2323  r19.26  2747  r19.40  2763  eqvinc  2967  reu6  3026  reu3  3027  unineq  3506  undif3  3516  un00  3587  uniintsn  3964  opkthg  4132  addcnnul  4454  preaddccan2  4456  ssfin  4471  ncfinprop  4475  tfinprop  4490  tfinltfin  4502  eventfin  4518  oddtfin  4519  sfindbl  4531  opth  4603  opexb  4604  opelopabsb  4698  ideqg  4869  ideqg2  4870  dminss  5042  imainss  5043  xpnz  5046  ssxpb  5056  funeu  5132  fun11uni  5163  funssxp  5234  ffdm  5235  f00  5250  dffo2  5274  fodmrnu  5278  foco  5280  fun11iun  5306  f1o00  5318  fv3  5342  dff2  5420  dff3  5421  dffo4  5424  ffnfv  5428  ffvresb  5432  fsn2  5435  fconstfv  5457  isocnv  5492  isotr  5496  extd  5924  symd  5925  mapsspm  6022  map0  6026  enadj  6061  enmap2lem3  6066  enmap2  6069  enmap1lem3  6072  enprmaplem3  6079  enprmaplem6  6082  elnc  6126  peano4nc  6151  ce0addcnnul  6180  sbthlem3  6206  nmembers1lem3  6271  nchoicelem17  6306