Theorem jcad 522

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jca2  523  jctild  535  jctird  536  ancld  560  ancrd  561  oplem1  1072  2eu1  2677  2eu1v  2678  disjxiun  5104  iss  6035  oneqmini  6415  funssres  6581  elpreima  7054  isomin  7342  oneqmin  7803  frxp  8128  soseq  8161  tposfo2  8251  oa00  8550  odi  8570  oneo  8572  oeordsuc  8586  oelim2  8587  nnarcl  8608  nnmord  8624  nnneo  8647  map0g  8895  pssnn  9167  fodomfib  9302  inf3lem4  9614  cplem1  9893  cplem1OLD  9894  kardenOLD  9903  alephordi  10081  cardinfima  10104  dfac5lem5  10134  isf34lem4  10383  axcc4  10445  axdc3lem2  10457  zorn2lem4  10505  zorn2lem7  10508  indpi  10920  genpcl  11021  addclprlem2  11030  ltaddpr  11047  ltexprlem5  11053  suplem1pr  11065  ltlen  11339  dedekind  11401  sup2  12199  nominpos  12509  uzind  12717  xrmaxlt  13237  xrltmin  13238  xrmaxle  13239  xrlemin  13240  xmullem2  13321  ccatopth  14789  shftuz  15146  sqreulem  15451  limsupbnd2  15574  mulcn2  15687  sadcaddlem  16553  dvdsgcdb  16641  algcvgblem  16673  lcmdvdsb  16709  rpexp  16819  infpnlem1  17008  divsfval  17639  iscatd  17767  posasymb  18413  plttr  18434  joinle  18478  meetle  18492  latnlej  18550  latnlej2  18553  lsmlub  19797  imasring  20477  unitmulclb  20528  lbspss  21272  lspsneu  21316  lspprat  21346  assapropd  22092  isclo2  23319  cncls2  23504  cncls  23505  cnntr  23506  cnrest2  23517  cmpsub  23631  cmpcld  23633  kgenss  23775  ptpjpre1  23803  txlm  23880  qtoptop2  23931  cmphaushmeo  24032  fbun  24072  isfild  24090  fbasrn  24116  fgtr  24122  ufinffr  24161  rnelfm  24185  fmfnfmlem4  24189  ghmcnp  24347  metrest  24756  icoopnst  25173  iocopnst  25174  dvfsumlem2  26261  dgreq0  26498  plyexmo  26552  taylthlem2  26617  cxpeq0  26923  mumullem2  27424  chpchtsum  27463  bposlem7  27534  lgsqr  27595  ltsres  27906  nosupno  27947  noinfno  27962  ltlesnd  28019  uspgr2wlkeq  30113  subgrwlk  30156  wwlknllvtx  30322  ex-natded5.3-2  30896  ubthlem1  31359  axhcompl-zf  31487  ococss  31782  nmopun  32503  elpjrn  32679  stm1addi  32734  stm1add3i  32736  mdsl1i  32810  chrelat2i  32854  atexch  32870  atcvat4i  32886  mdsymlem3  32894  bnj600  35436  trssfir1om  35629  trssfir1omregs  35670  karddom  35695  kardsdom  35696  pthacycspth  35744  subfacval2  35774  climuzcnv  36258  3jcadALT  36274  fundmpss  36354  segconeq  36598  ifscgr  36632  endofsegid  36673  colinbtwnle  36706  trer  36943  ivthALT  36962  fnessref  36984  fnemeet2  36994  fnejoin2  36996  onsuct0  37068  bj-ideqg1  37924  bj-elid6  37930  bj-finsumval0  38045  bj-isrvec2  38060  bj-bary1  38072  icorempo  38113  isbasisrelowllem1  38117  isbasisrelowllem2  38118  relowlpssretop  38126  finxpsuclem  38159  pibt2  38179  poimirlem31  38408  isbnd2  38541  bfplem2  38581  ghomco  38649  cnf1dd  38846  contrd  38853  mpobi123f  38918  mptbi12f  38922  iss2  39100  refressn  39289  jca2r  39736  prter2  39762  lshpset2N  40000  cvrnbtwn2  40156  cvrnbtwn3  40157  cvrnbtwn4  40160  cvlcvr1  40220  hlrelat2  40284  cvrat4  40324  islpln2a  40429  linepsubN  40633  elpaddn0  40681  paddssw2  40725  pmapjoin  40733  ispsubcl2N  40828  dochkrshp  42267  dochsatshp  42332  mapdh9a  42670  hdmap11lem2  42723  sn-sup2  43387  frlmfzowrdb  43400  pwinfi3  44411  clsk1independent  44894  gneispace  44982  pm11.71  45229  relpmin  45783  ormkglobd  47713  2reu8i  48009  sbgoldbaltlem2  48704  oppcendc  49952  setrec1lem4  50624