Theorem jcad 513

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  jca2  514  jctild  526  jctird  527  ancld  551  ancrd  552  oplem1  1054  2eu1  2653  2eu1v  2654  disjxiun  5072  iss  5946  oneqmini  6321  funssres  6485  elpreima  6944  isomin  7217  oneqmin  7659  frxp  7976  tposfo2  8074  oa00  8399  odi  8419  oneo  8421  oeordsuc  8434  oelim2  8435  nnarcl  8456  nnmord  8472  nnneo  8494  map0g  8681  pssnn  8960  onomeneqOLD  9021  pssnnOLD  9049  fodomfib  9102  inf3lem4  9398  cplem1  9656  karden  9662  alephordi  9839  cardinfima  9862  dfac5lem5  9892  isf34lem4  10142  axcc4  10204  axdc3lem2  10216  zorn2lem4  10264  zorn2lem7  10267  indpi  10672  genpcl  10773  addclprlem2  10782  ltaddpr  10799  ltexprlem5  10805  suplem1pr  10817  ltlen  11085  dedekind  11147  mulgt1  11843  sup2  11940  nominpos  12219  uzind  12421  xrmaxlt  12924  xrltmin  12925  xrmaxle  12926  xrlemin  12927  xmullem2  13008  ccatopth  14438  shftuz  14789  sqreulem  15080  limsupbnd2  15201  mulcn2  15314  sadcaddlem  16173  dvdsgcdb  16262  algcvgblem  16291  lcmdvdsb  16327  rpexp  16436  infpnlem1  16620  divsfval  17267  iscatd  17391  posasymb  18046  plttr  18069  joinle  18113  meetle  18127  latnlej  18183  latnlej2  18186  lsmlub  19279  imasring  19867  unitmulclb  19916  lbspss  20353  lspsneu  20394  lspprat  20424  assapropd  21085  isclo2  22248  cncls2  22433  cncls  22434  cnntr  22435  cnrest2  22446  cmpsub  22560  cmpcld  22562  kgenss  22703  ptpjpre1  22731  txlm  22808  qtoptop2  22859  cmphaushmeo  22960  fbun  23000  isfild  23018  fbasrn  23044  fgtr  23050  ufinffr  23089  rnelfm  23113  fmfnfmlem4  23117  ghmcnp  23275  metrest  23689  icoopnst  24111  iocopnst  24112  dgreq0  25435  plyexmo  25482  cxpeq0  25842  mumullem2  26338  chpchtsum  26376  bposlem7  26447  lgsqr  26508  uspgr2wlkeq  28022  wwlknllvtx  28220  ex-natded5.3-2  28781  ubthlem1  29241  axhcompl-zf  29369  ococss  29664  nmopun  30385  elpjrn  30561  stm1addi  30616  stm1add3i  30618  mdsl1i  30692  chrelat2i  30736  atexch  30752  atcvat4i  30768  mdsymlem3  30776  bian1d  30818  bnj600  32908  subgrwlk  33103  pthacycspth  33128  subfacval2  33158  climuzcnv  33638  fundmpss  33749  soseq  33812  sltres  33874  nosupno  33915  noinfno  33930  segconeq  34321  ifscgr  34355  endofsegid  34396  colinbtwnle  34429  trer  34514  ivthALT  34533  fnessref  34555  fnemeet2  34565  fnejoin2  34567  onsuct0  34639  bj-ideqg1  35344  bj-elid6  35350  bj-finsumval0  35465  bj-isrvec2  35480  bj-bary1  35492  icorempo  35531  isbasisrelowllem1  35535  isbasisrelowllem2  35536  relowlpssretop  35544  finxpsuclem  35577  pibt2  35597  poimirlem31  35817  isbnd2  35950  bfplem2  35990  ghomco  36058  cnf1dd  36257  contrd  36264  mpobi123f  36329  mptbi12f  36333  iss2  36486  jca2r  36876  prter2  36902  lshpset2N  37140  cvrnbtwn2  37296  cvrnbtwn3  37297  cvrnbtwn4  37300  cvlcvr1  37360  hlrelat2  37424  cvrat4  37464  islpln2a  37569  linepsubN  37773  elpaddn0  37821  paddssw2  37865  pmapjoin  37873  ispsubcl2N  37968  dochkrshp  39407  dochsatshp  39472  mapdh9a  39810  hdmap11lem2  39863  frlmfzowrdb  40242  sn-sup2  40446  pwinfi3  41177  clsk1independent  41663  gneispace  41751  pm11.71  42022  2reu8i  44616  sbgoldbaltlem2  45243  setrec1lem4  46407  tworepnotupword  46532