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-1 5  ax-2 6  ax-3 7  ax-mp 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  2746  r19.40  2762  eqvinc  2966  reu6  3025  reu3  3026  unineq  3505  undif3  3515  un00  3586  uniintsn  3963  opkthg  4131  addcnnul  4453  preaddccan2  4455  ssfin  4470  ncfinprop  4474  tfinprop  4489  tfinltfin  4501  eventfin  4517  oddtfin  4518  sfindbl  4530  opth  4602  opexb  4603  opelopabsb  4697  ideqg  4868  ideqg2  4869  dminss  5041  imainss  5042  xpnz  5045  ssxpb  5055  funeu  5131  fun11uni  5162  funssxp  5233  ffdm  5234  f00  5249  dffo2  5273  fodmrnu  5277  foco  5279  fun11iun  5305  f1o00  5317  fv3  5341  dff2  5419  dff3  5420  dffo4  5423  ffnfv  5427  ffvresb  5431  fsn2  5434  fconstfv  5456  isocnv  5491  isotr  5495  extd  5923  symd  5924  mapsspm  6021  map0  6025  enadj  6060  enmap2lem3  6065  enmap2  6068  enmap1lem3  6071  enprmaplem3  6078  enprmaplem6  6081  elnc  6125  peano4nc  6150  ce0addcnnul  6179  sbthlem3  6205  nmembers1lem3  6270  nchoicelem17  6305