Theorem jcad 521

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  jca2  522  jctild  534  jctird  535  ancld  559  ancrd  560  oplem1  1070  2eu1  2680  2eu1v  2681  disjxiun  5102  iss  6028  oneqmini  6403  funssres  6569  elpreima  7043  isomin  7325  oneqmin  7787  frxp  8110  soseq  8143  tposfo2  8233  oa00  8532  odi  8552  oneo  8554  oeordsuc  8568  oelim2  8569  nnarcl  8590  nnmord  8606  nnneo  8629  map0g  8870  pssnn  9141  fodomfib  9276  inf3lem4  9588  cplem1  9863  karden  9869  alephordi  10046  cardinfima  10069  dfac5lem5  10099  isf34lem4  10349  axcc4  10411  axdc3lem2  10423  zorn2lem4  10471  zorn2lem7  10474  indpi  10880  genpcl  10981  addclprlem2  10990  ltaddpr  11007  ltexprlem5  11013  suplem1pr  11025  ltlen  11299  dedekind  11361  sup2  12162  nominpos  12472  uzind  12679  xrmaxlt  13198  xrltmin  13199  xrmaxle  13200  xrlemin  13201  xmullem2  13282  ccatopth  14743  shftuz  15096  sqreulem  15401  limsupbnd2  15524  mulcn2  15637  sadcaddlem  16505  dvdsgcdb  16593  algcvgblem  16625  lcmdvdsb  16661  rpexp  16771  infpnlem1  16960  divsfval  17591  iscatd  17719  posasymb  18365  plttr  18386  joinle  18430  meetle  18444  latnlej  18502  latnlej2  18505  lsmlub  19725  imasring  20403  unitmulclb  20454  lbspss  21172  lspsneu  21216  lspprat  21246  assapropd  21981  isclo2  23206  cncls2  23391  cncls  23392  cnntr  23393  cnrest2  23404  cmpsub  23518  cmpcld  23520  kgenss  23661  ptpjpre1  23689  txlm  23766  qtoptop2  23817  cmphaushmeo  23918  fbun  23958  isfild  23976  fbasrn  24002  fgtr  24008  ufinffr  24047  rnelfm  24071  fmfnfmlem4  24075  ghmcnp  24233  metrest  24642  icoopnst  25059  iocopnst  25060  dvfsumlem2  26147  dgreq0  26383  plyexmo  26435  taylthlem2  26495  cxpeq0  26801  mumullem2  27302  chpchtsum  27341  bposlem7  27412  lgsqr  27473  ltsres  27784  nosupno  27825  noinfno  27840  ltlesnd  27897  uspgr2wlkeq  29904  wwlknllvtx  30104  ex-natded5.3-2  30668  ubthlem1  31131  axhcompl-zf  31259  ococss  31554  nmopun  32275  elpjrn  32451  stm1addi  32506  stm1add3i  32508  mdsl1i  32582  chrelat2i  32626  atexch  32642  atcvat4i  32658  mdsymlem3  32666  bnj600  35224  trssfir1om  35419  trssfir1omregs  35444  subgrwlk  35495  pthacycspth  35520  subfacval2  35550  climuzcnv  36034  3jcadALT  36050  fundmpss  36130  segconeq  36373  ifscgr  36407  endofsegid  36448  colinbtwnle  36481  trer  36689  ivthALT  36708  fnessref  36730  fnemeet2  36740  fnejoin2  36742  onsuct0  36814  bj-ideqg1  37668  bj-elid6  37674  bj-finsumval0  37789  bj-isrvec2  37804  bj-bary1  37816  icorempo  37857  isbasisrelowllem1  37861  isbasisrelowllem2  37862  relowlpssretop  37870  finxpsuclem  37903  pibt2  37923  poimirlem31  38162  isbnd2  38294  bfplem2  38334  ghomco  38402  cnf1dd  38601  contrd  38608  mpobi123f  38673  mptbi12f  38677  iss2  38855  refressn  39044  jca2r  39491  prter2  39517  lshpset2N  39755  cvrnbtwn2  39911  cvrnbtwn3  39912  cvrnbtwn4  39915  cvlcvr1  39975  hlrelat2  40039  cvrat4  40079  islpln2a  40184  linepsubN  40388  elpaddn0  40436  paddssw2  40480  pmapjoin  40488  ispsubcl2N  40583  dochkrshp  42022  dochsatshp  42087  mapdh9a  42425  hdmap11lem2  42478  sn-sup2  43125  frlmfzowrdb  43138  pwinfi3  44151  clsk1independent  44634  gneispace  44722  pm11.71  44971  relpmin  45526  ormkglobd  47449  2reu8i  47705  sbgoldbaltlem2  48400  oppcendc  49647  setrec1lem4  50319