Theorem jcad 516

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 515 and double deduction form of pm3.2 473 and pm3.2i 474. (Contributed by NM, 15-Jul-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 473	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 70	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  jca2  517  jctild  529  jctird  530  ancld  554  ancrd  555  oplem1  1057  2eu1  2651  2eu1v  2652  disjxiun  5050  iss  5903  oneqmini  6264  funssres  6424  elpreima  6878  isomin  7146  oneqmin  7584  frxp  7893  tposfo2  7991  oa00  8287  odi  8307  oneo  8309  oeordsuc  8322  oelim2  8323  nnarcl  8344  nnmord  8360  nnneo  8380  map0g  8565  pssnn  8846  onomeneq  8869  pssnnOLD  8895  fodomfib  8950  inf3lem4  9246  cplem1  9505  karden  9511  alephordi  9688  cardinfima  9711  dfac5lem5  9741  isf34lem4  9991  axcc4  10053  axdc3lem2  10065  zorn2lem4  10113  zorn2lem7  10116  indpi  10521  genpcl  10622  addclprlem2  10631  ltaddpr  10648  ltexprlem5  10654  suplem1pr  10666  ltlen  10933  dedekind  10995  mulgt1  11691  sup2  11788  nominpos  12067  uzind  12269  xrmaxlt  12771  xrltmin  12772  xrmaxle  12773  xrlemin  12774  xmullem2  12855  ccatopth  14281  shftuz  14632  sqreulem  14923  limsupbnd2  15044  mulcn2  15157  sadcaddlem  16016  dvdsgcdb  16105  algcvgblem  16134  lcmdvdsb  16170  rpexp  16279  infpnlem1  16463  divsfval  17052  iscatd  17176  posasymb  17826  plttr  17848  joinle  17892  meetle  17906  latnlej  17962  latnlej2  17965  lsmlub  19054  imasring  19637  unitmulclb  19683  lbspss  20119  lspsneu  20160  lspprat  20190  assapropd  20831  isclo2  21985  cncls2  22170  cncls  22171  cnntr  22172  cnrest2  22183  cmpsub  22297  cmpcld  22299  kgenss  22440  ptpjpre1  22468  txlm  22545  qtoptop2  22596  cmphaushmeo  22697  fbun  22737  isfild  22755  fbasrn  22781  fgtr  22787  ufinffr  22826  rnelfm  22850  fmfnfmlem4  22854  ghmcnp  23012  metrest  23422  icoopnst  23836  iocopnst  23837  dgreq0  25159  plyexmo  25206  cxpeq0  25566  mumullem2  26062  chpchtsum  26100  bposlem7  26171  lgsqr  26232  uspgr2wlkeq  27733  wwlknllvtx  27930  ex-natded5.3-2  28491  ubthlem1  28951  axhcompl-zf  29079  ococss  29374  nmopun  30095  elpjrn  30271  stm1addi  30326  stm1add3i  30328  mdsl1i  30402  chrelat2i  30446  atexch  30462  atcvat4i  30478  mdsymlem3  30486  bian1d  30528  bnj600  32612  subgrwlk  32807  pthacycspth  32832  subfacval2  32862  climuzcnv  33342  fundmpss  33459  soseq  33540  sltres  33602  nosupno  33643  noinfno  33658  segconeq  34049  ifscgr  34083  endofsegid  34124  colinbtwnle  34157  trer  34242  ivthALT  34261  fnessref  34283  fnemeet2  34293  fnejoin2  34295  onsuct0  34367  bj-ideqg1  35070  bj-elid6  35076  bj-finsumval0  35191  bj-isrvec2  35205  bj-bary1  35217  icorempo  35259  isbasisrelowllem1  35263  isbasisrelowllem2  35264  relowlpssretop  35272  finxpsuclem  35305  pibt2  35325  poimirlem31  35545  isbnd2  35678  bfplem2  35718  ghomco  35786  cnf1dd  35985  contrd  35992  mpobi123f  36057  mptbi12f  36061  iss2  36216  jca2r  36606  prter2  36632  lshpset2N  36870  cvrnbtwn2  37026  cvrnbtwn3  37027  cvrnbtwn4  37030  cvlcvr1  37090  hlrelat2  37154  cvrat4  37194  islpln2a  37299  linepsubN  37503  elpaddn0  37551  paddssw2  37595  pmapjoin  37603  ispsubcl2N  37698  dochkrshp  39137  dochsatshp  39202  mapdh9a  39540  hdmap11lem2  39593  frlmfzowrdb  39948  sn-sup2  40147  pwinfi3  40846  clsk1independent  41333  gneispace  41421  pm11.71  41688  2reu8i  44277  sbgoldbaltlem2  44905  setrec1lem4  46067