Theorem jcad 512

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  jca2  513  jctild  525  jctird  526  ancld  550  ancrd  551  oplem1  1053  2eu1  2653  2eu1v  2654  disjxiun  5075  iss  5940  oneqmini  6314  funssres  6474  elpreima  6929  isomin  7201  oneqmin  7640  frxp  7951  tposfo2  8049  oa00  8366  odi  8386  oneo  8388  oeordsuc  8401  oelim2  8402  nnarcl  8423  nnmord  8439  nnneo  8459  map0g  8646  pssnn  8916  onomeneq  8975  pssnnOLD  9001  fodomfib  9054  inf3lem4  9350  cplem1  9631  karden  9637  alephordi  9814  cardinfima  9837  dfac5lem5  9867  isf34lem4  10117  axcc4  10179  axdc3lem2  10191  zorn2lem4  10239  zorn2lem7  10242  indpi  10647  genpcl  10748  addclprlem2  10757  ltaddpr  10774  ltexprlem5  10780  suplem1pr  10792  ltlen  11059  dedekind  11121  mulgt1  11817  sup2  11914  nominpos  12193  uzind  12395  xrmaxlt  12897  xrltmin  12898  xrmaxle  12899  xrlemin  12900  xmullem2  12981  ccatopth  14410  shftuz  14761  sqreulem  15052  limsupbnd2  15173  mulcn2  15286  sadcaddlem  16145  dvdsgcdb  16234  algcvgblem  16263  lcmdvdsb  16299  rpexp  16408  infpnlem1  16592  divsfval  17239  iscatd  17363  posasymb  18018  plttr  18041  joinle  18085  meetle  18099  latnlej  18155  latnlej2  18158  lsmlub  19251  imasring  19839  unitmulclb  19888  lbspss  20325  lspsneu  20366  lspprat  20396  assapropd  21057  isclo2  22220  cncls2  22405  cncls  22406  cnntr  22407  cnrest2  22418  cmpsub  22532  cmpcld  22534  kgenss  22675  ptpjpre1  22703  txlm  22780  qtoptop2  22831  cmphaushmeo  22932  fbun  22972  isfild  22990  fbasrn  23016  fgtr  23022  ufinffr  23061  rnelfm  23085  fmfnfmlem4  23089  ghmcnp  23247  metrest  23661  icoopnst  24083  iocopnst  24084  dgreq0  25407  plyexmo  25454  cxpeq0  25814  mumullem2  26310  chpchtsum  26348  bposlem7  26419  lgsqr  26480  uspgr2wlkeq  27993  wwlknllvtx  28190  ex-natded5.3-2  28751  ubthlem1  29211  axhcompl-zf  29339  ococss  29634  nmopun  30355  elpjrn  30531  stm1addi  30586  stm1add3i  30588  mdsl1i  30662  chrelat2i  30706  atexch  30722  atcvat4i  30738  mdsymlem3  30746  bian1d  30788  bnj600  32878  subgrwlk  33073  pthacycspth  33098  subfacval2  33128  climuzcnv  33608  fundmpss  33719  soseq  33782  sltres  33844  nosupno  33885  noinfno  33900  segconeq  34291  ifscgr  34325  endofsegid  34366  colinbtwnle  34399  trer  34484  ivthALT  34503  fnessref  34525  fnemeet2  34535  fnejoin2  34537  onsuct0  34609  bj-ideqg1  35314  bj-elid6  35320  bj-finsumval0  35435  bj-isrvec2  35450  bj-bary1  35462  icorempo  35501  isbasisrelowllem1  35505  isbasisrelowllem2  35506  relowlpssretop  35514  finxpsuclem  35547  pibt2  35567  poimirlem31  35787  isbnd2  35920  bfplem2  35960  ghomco  36028  cnf1dd  36227  contrd  36234  mpobi123f  36299  mptbi12f  36303  iss2  36458  jca2r  36848  prter2  36874  lshpset2N  37112  cvrnbtwn2  37268  cvrnbtwn3  37269  cvrnbtwn4  37272  cvlcvr1  37332  hlrelat2  37396  cvrat4  37436  islpln2a  37541  linepsubN  37745  elpaddn0  37793  paddssw2  37837  pmapjoin  37845  ispsubcl2N  37940  dochkrshp  39379  dochsatshp  39444  mapdh9a  39782  hdmap11lem2  39835  frlmfzowrdb  40215  sn-sup2  40419  pwinfi3  41123  clsk1independent  41609  gneispace  41697  pm11.71  41968  2reu8i  44556  sbgoldbaltlem2  45184  setrec1lem4  46348