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  1072  2eu1  2678  2eu1v  2679  disjxiun  5107  iss  6039  oneqmini  6416  funssres  6582  elpreima  7055  isomin  7337  oneqmin  7800  frxp  8123  soseq  8156  tposfo2  8246  oa00  8545  odi  8565  oneo  8567  oeordsuc  8581  oelim2  8582  nnarcl  8603  nnmord  8619  nnneo  8642  map0g  8883  pssnn  9154  fodomfib  9289  inf3lem4  9601  cplem1  9876  karden  9882  alephordi  10059  cardinfima  10082  dfac5lem5  10112  isf34lem4  10362  axcc4  10424  axdc3lem2  10436  zorn2lem4  10484  zorn2lem7  10487  indpi  10893  genpcl  10994  addclprlem2  11003  ltaddpr  11020  ltexprlem5  11026  suplem1pr  11038  ltlen  11312  dedekind  11374  sup2  12172  nominpos  12482  uzind  12689  xrmaxlt  13208  xrltmin  13209  xrmaxle  13210  xrlemin  13211  xmullem2  13292  ccatopth  14755  shftuz  15108  sqreulem  15413  limsupbnd2  15536  mulcn2  15649  sadcaddlem  16516  dvdsgcdb  16604  algcvgblem  16636  lcmdvdsb  16672  rpexp  16782  infpnlem1  16971  divsfval  17602  iscatd  17730  posasymb  18376  plttr  18397  joinle  18441  meetle  18455  latnlej  18513  latnlej2  18516  lsmlub  19735  imasring  20413  unitmulclb  20464  lbspss  21184  lspsneu  21228  lspprat  21258  assapropd  22002  isclo2  23226  cncls2  23411  cncls  23412  cnntr  23413  cnrest2  23424  cmpsub  23538  cmpcld  23540  kgenss  23681  ptpjpre1  23709  txlm  23786  qtoptop2  23837  cmphaushmeo  23938  fbun  23978  isfild  23996  fbasrn  24022  fgtr  24028  ufinffr  24067  rnelfm  24091  fmfnfmlem4  24095  ghmcnp  24253  metrest  24662  icoopnst  25079  iocopnst  25080  dvfsumlem2  26167  dgreq0  26403  plyexmo  26455  taylthlem2  26515  cxpeq0  26821  mumullem2  27322  chpchtsum  27361  bposlem7  27432  lgsqr  27493  ltsres  27804  nosupno  27845  noinfno  27860  ltlesnd  27917  uspgr2wlkeq  29973  wwlknllvtx  30173  ex-natded5.3-2  30737  ubthlem1  31200  axhcompl-zf  31328  ococss  31623  nmopun  32344  elpjrn  32520  stm1addi  32575  stm1add3i  32577  mdsl1i  32651  chrelat2i  32695  atexch  32711  atcvat4i  32727  mdsymlem3  32735  bnj600  35285  trssfir1om  35485  trssfir1omregs  35527  karddom  35552  kardsdom  35553  subgrwlk  35602  pthacycspth  35627  subfacval2  35657  climuzcnv  36141  3jcadALT  36157  fundmpss  36237  segconeq  36480  ifscgr  36514  endofsegid  36555  colinbtwnle  36588  trer  36805  ivthALT  36824  fnessref  36846  fnemeet2  36856  fnejoin2  36858  onsuct0  36930  bj-ideqg1  37786  bj-elid6  37792  bj-finsumval0  37907  bj-isrvec2  37922  bj-bary1  37934  icorempo  37975  isbasisrelowllem1  37979  isbasisrelowllem2  37980  relowlpssretop  37988  finxpsuclem  38021  pibt2  38041  poimirlem31  38280  isbnd2  38412  bfplem2  38452  ghomco  38520  cnf1dd  38717  contrd  38724  mpobi123f  38789  mptbi12f  38793  iss2  38971  refressn  39160  jca2r  39607  prter2  39633  lshpset2N  39871  cvrnbtwn2  40027  cvrnbtwn3  40028  cvrnbtwn4  40031  cvlcvr1  40091  hlrelat2  40155  cvrat4  40195  islpln2a  40300  linepsubN  40504  elpaddn0  40552  paddssw2  40596  pmapjoin  40604  ispsubcl2N  40699  dochkrshp  42138  dochsatshp  42203  mapdh9a  42541  hdmap11lem2  42594  sn-sup2  43243  frlmfzowrdb  43256  pwinfi3  44269  clsk1independent  44752  gneispace  44840  pm11.71  45087  relpmin  45641  ormkglobd  47571  2reu8i  47827  sbgoldbaltlem2  48522  oppcendc  49773  setrec1lem4  50445