Theorem jcad 515

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  jca2  516  jctild  528  jctird  529  ancld  553  ancrd  554  oplem1  1051  2eu1  2735  2eu1v  2736  disjxiun  5065  iss  5905  oneqmini  6244  funssres  6400  elpreima  6830  isomin  7092  oneqmin  7522  frxp  7822  tposfo2  7917  oa00  8187  odi  8207  oneo  8209  oeordsuc  8222  oelim2  8223  nnarcl  8244  nnmord  8260  nnneo  8280  map0g  8450  onomeneq  8710  pssnn  8738  fodomfib  8800  inf3lem4  9096  cplem1  9320  karden  9326  alephordi  9502  cardinfima  9525  dfac5lem5  9555  isf34lem4  9801  axcc4  9863  axdc3lem2  9875  zorn2lem4  9923  zorn2lem7  9926  indpi  10331  genpcl  10432  addclprlem2  10441  ltaddpr  10458  ltexprlem5  10464  suplem1pr  10476  ltlen  10743  dedekind  10805  mulgt1  11501  sup2  11599  nominpos  11877  uzind  12077  xrmaxlt  12577  xrltmin  12578  xrmaxle  12579  xrlemin  12580  xmullem2  12661  ccatopth  14080  shftuz  14430  sqreulem  14721  limsupbnd2  14842  mulcn2  14954  sadcaddlem  15808  dvdsgcdb  15895  algcvgblem  15923  lcmdvdsb  15959  rpexp  16066  infpnlem1  16248  divsfval  16822  iscatd  16946  posasymb  17564  plttr  17582  joinle  17626  meetle  17640  latnlej  17680  latnlej2  17683  lsmlub  18792  imasring  19371  unitmulclb  19417  lbspss  19856  lspsneu  19897  lspprat  19927  assapropd  20103  isclo2  21698  cncls2  21883  cncls  21884  cnntr  21885  cnrest2  21896  cmpsub  22010  cmpcld  22012  kgenss  22153  ptpjpre1  22181  txlm  22258  qtoptop2  22309  cmphaushmeo  22410  fbun  22450  isfild  22468  fbasrn  22494  fgtr  22500  ufinffr  22539  rnelfm  22563  fmfnfmlem4  22567  ghmcnp  22725  metrest  23136  icoopnst  23545  iocopnst  23546  dgreq0  24857  plyexmo  24904  cxpeq0  25263  mumullem2  25759  chpchtsum  25797  bposlem7  25868  lgsqr  25929  uspgr2wlkeq  27429  wwlknllvtx  27626  ex-natded5.3-2  28189  ubthlem1  28649  axhcompl-zf  28777  ococss  29072  nmopun  29793  elpjrn  29969  stm1addi  30024  stm1add3i  30026  mdsl1i  30100  chrelat2i  30144  atexch  30160  atcvat4i  30176  mdsymlem3  30184  bian1d  30226  bnj600  32193  subgrwlk  32381  pthacycspth  32406  subfacval2  32436  climuzcnv  32916  fundmpss  33011  soseq  33098  sltres  33171  nosupno  33205  segconeq  33473  ifscgr  33507  endofsegid  33548  colinbtwnle  33581  trer  33666  ivthALT  33685  fnessref  33707  fnemeet2  33717  fnejoin2  33719  onsuct0  33791  bj-ideqg1  34458  bj-elid6  34464  bj-finsumval0  34569  bj-isrvec2  34583  bj-bary1  34595  icorempo  34634  isbasisrelowllem1  34638  isbasisrelowllem2  34639  relowlpssretop  34647  finxpsuclem  34680  pibt2  34700  poimirlem31  34925  isbnd2  35063  bfplem2  35103  ghomco  35171  cnf1dd  35370  contrd  35377  mpobi123f  35442  mptbi12f  35446  iss2  35603  jca2r  35993  prter2  36019  lshpset2N  36257  cvrnbtwn2  36413  cvrnbtwn3  36414  cvrnbtwn4  36417  cvlcvr1  36477  hlrelat2  36541  cvrat4  36581  islpln2a  36686  linepsubN  36890  elpaddn0  36938  paddssw2  36982  pmapjoin  36990  ispsubcl2N  37085  dochkrshp  38524  dochsatshp  38589  mapdh9a  38927  hdmap11lem2  38980  frlmfzowrdb  39150  pwinfi3  39929  clsk1independent  40403  gneispace  40491  pm11.71  40736  2reu8i  43319  sbgoldbaltlem2  43952  setrec1lem4  44800