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

This theorem is referenced by:  jca2  513  jctild  525  jctird  526  ancld  550  ancrd  551  oplem1  1056  2eu1  2651  2eu1v  2652  disjxiun  5121  iss  6027  oneqmini  6410  funssres  6585  elpreima  7053  isomin  7335  oneqmin  7799  frxp  8130  soseq  8163  tposfo2  8253  oa00  8576  odi  8596  oneo  8598  oeordsuc  8611  oelim2  8612  nnarcl  8633  nnmord  8649  nnneo  8672  map0g  8903  pssnn  9187  onomeneqOLD  9243  fodomfib  9346  fodomfibOLD  9348  inf3lem4  9650  cplem1  9908  karden  9914  alephordi  10093  cardinfima  10116  dfac5lem5  10146  isf34lem4  10396  axcc4  10458  axdc3lem2  10470  zorn2lem4  10518  zorn2lem7  10521  indpi  10926  genpcl  11027  addclprlem2  11036  ltaddpr  11053  ltexprlem5  11059  suplem1pr  11071  ltlen  11341  dedekind  11403  mulgt1OLD  12105  sup2  12203  nominpos  12483  uzind  12690  xrmaxlt  13202  xrltmin  13203  xrmaxle  13204  xrlemin  13205  xmullem2  13286  ccatopth  14739  shftuz  15093  sqreulem  15383  limsupbnd2  15504  mulcn2  15617  sadcaddlem  16481  dvdsgcdb  16569  algcvgblem  16601  lcmdvdsb  16637  rpexp  16746  infpnlem1  16935  divsfval  17566  iscatd  17690  posasymb  18336  plttr  18357  joinle  18401  meetle  18415  latnlej  18471  latnlej2  18474  lsmlub  19650  imasring  20295  unitmulclb  20346  lbspss  21045  lspsneu  21089  lspprat  21119  assapropd  21837  isclo2  23031  cncls2  23216  cncls  23217  cnntr  23218  cnrest2  23229  cmpsub  23343  cmpcld  23345  kgenss  23486  ptpjpre1  23514  txlm  23591  qtoptop2  23642  cmphaushmeo  23743  fbun  23783  isfild  23801  fbasrn  23827  fgtr  23833  ufinffr  23872  rnelfm  23896  fmfnfmlem4  23900  ghmcnp  24058  metrest  24468  icoopnst  24892  iocopnst  24893  dvfsumlem2  25990  dgreq0  26228  plyexmo  26278  taylthlem2  26339  cxpeq0  26644  mumullem2  27147  chpchtsum  27187  bposlem7  27258  lgsqr  27319  sltres  27631  nosupno  27672  noinfno  27687  sltlend  27740  uspgr2wlkeq  29631  wwlknllvtx  29833  ex-natded5.3-2  30394  ubthlem1  30856  axhcompl-zf  30984  ococss  31279  nmopun  32000  elpjrn  32176  stm1addi  32231  stm1add3i  32233  mdsl1i  32307  chrelat2i  32351  atexch  32367  atcvat4i  32383  mdsymlem3  32391  bian1dOLD  32443  bnj600  34955  subgrwlk  35159  pthacycspth  35184  subfacval2  35214  climuzcnv  35698  3jcadALT  35714  fundmpss  35789  segconeq  36033  ifscgr  36067  endofsegid  36108  colinbtwnle  36141  trer  36339  ivthALT  36358  fnessref  36380  fnemeet2  36390  fnejoin2  36392  onsuct0  36464  bj-ideqg1  37187  bj-elid6  37193  bj-finsumval0  37308  bj-isrvec2  37323  bj-bary1  37335  icorempo  37374  isbasisrelowllem1  37378  isbasisrelowllem2  37379  relowlpssretop  37387  finxpsuclem  37420  pibt2  37440  poimirlem31  37680  isbnd2  37812  bfplem2  37852  ghomco  37920  cnf1dd  38119  contrd  38126  mpobi123f  38191  mptbi12f  38195  iss2  38367  refressn  38466  jca2r  38878  prter2  38904  lshpset2N  39142  cvrnbtwn2  39298  cvrnbtwn3  39299  cvrnbtwn4  39302  cvlcvr1  39362  hlrelat2  39427  cvrat4  39467  islpln2a  39572  linepsubN  39776  elpaddn0  39824  paddssw2  39868  pmapjoin  39876  ispsubcl2N  39971  dochkrshp  41410  dochsatshp  41475  mapdh9a  41813  hdmap11lem2  41866  sn-sup2  42489  frlmfzowrdb  42502  pwinfi3  43562  clsk1independent  44045  gneispace  44133  pm11.71  44396  relpmin  44952  ormkglobd  46884  tworepnotupword  46895  2reu8i  47122  sbgoldbaltlem2  47774  oppcendc  48973  setrec1lem4  49534