Theorem jcad 508

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  jca2  509  jctild  521  jctird  522  ancld  546  ancrd  547  anim12ii  611  oplem1  1079  2eu1  2675  rr19.28v  3500  disjxiun  4806  iss  5624  preddowncl  5892  oneqmini  5959  funssres  6111  ssimaex  6452  elpreima  6527  isomin  6779  oneqmin  7203  frxp  7489  tposfo2  7578  onfununi  7642  oaordex  7843  oa00  7844  odi  7864  oneo  7866  oeordsuc  7879  oelim2  7880  nnarcl  7901  nnmord  7917  nnneo  7936  map0g  8101  domtriord  8313  onomeneq  8357  pssnn  8385  findcard3  8410  unfilem1  8431  fodomfib  8447  inf0  8733  inf3lem3  8742  inf3lem4  8743  tcel  8836  cplem1  8967  karden  8973  fidomtri2  9071  alephordi  9148  cardinfima  9171  alephval3  9184  dfac5lem5  9201  isf34lem4  9452  axcc4  9514  axdc3lem2  9526  zorn2lem4  9574  zorn2lem6  9576  zorn2lem7  9577  fodomb  9601  indpi  9982  genpcl  10083  addclprlem2  10092  ltaddpr  10109  ltexprlem5  10115  suplem1pr  10127  ltlen  10392  dedekind  10454  mulgt1  11136  sup2  11233  nominpos  11515  uzind  11716  eqreznegel  11975  xrmaxlt  12214  xrltmin  12215  xrmaxle  12216  xrlemin  12217  xmullem2  12297  ccatopth  13712  ccatopthOLD  13713  shftuz  14094  sqreulem  14384  limsupbnd2  14499  mulcn2  14611  sadcaddlem  15460  dvdsgcdb  15543  algcvgblem  15571  lcmdvdsb  15607  rpexp  15711  infpnlem1  15893  divsfval  16473  iscatd  16599  posasymb  17218  plttr  17236  joinle  17280  meetle  17294  latnlej  17334  latnlej2  17337  lsmlub  18342  imasring  18886  unitmulclb  18932  lbspss  19354  lspsneu  19395  lspprat  19427  assapropd  19601  isclo2  21172  cncls2  21357  cncls  21358  cnntr  21359  cnrest2  21370  cmpsub  21483  cmpcld  21485  kgenss  21626  ptpjpre1  21654  txcn  21709  txlm  21731  qtoptop2  21782  cmphaushmeo  21883  fbun  21923  isfild  21941  ssfg  21955  fbasrn  21967  fgtr  21973  ufinffr  22012  rnelfm  22036  fmfnfmlem4  22040  fclsnei  22102  ghmcnp  22197  metrest  22608  icoopnst  23017  iocopnst  23018  dgreq0  24312  plyexmo  24359  cxpeq0  24715  eldmgm  25039  mumullem2  25197  chpchtsum  25235  bposlem7  25306  lgsqr  25367  uspgr2wlkeq  26833  wwlknllvtx  27032  ex-natded5.3-2  27724  ubthlem1  28182  axhcompl-zf  28311  ococss  28608  nmopun  29329  elpjrn  29505  stm1addi  29560  stm1add3i  29562  mdsl1i  29636  chrelat2i  29680  atexch  29696  atcvat4i  29712  mdsymlem3  29720  bian1d  29762  bnj600  31437  subfacval2  31617  climuzcnv  32011  fundmpss  32109  soseq  32198  sltres  32259  nosupno  32293  segconeq  32561  ifscgr  32595  endofsegid  32636  colinbtwnle  32669  trer  32754  ivthALT  32773  fnessref  32795  fnemeet2  32805  fnejoin2  32807  onsuct0  32879  bj-finsumval0  33581  bj-bary1  33596  icorempt2  33632  isbasisrelowllem1  33636  isbasisrelowllem2  33637  relowlpssretop  33645  finxpsuclem  33667  poimirlem31  33864  isbnd2  34004  bfplem2  34044  ghomco  34112  cnf1dd  34314  contrd  34321  mpt2bi123f  34392  mptbi12f  34396  iss2  34541  jca2r  34810  prter2  34837  lshpset2N  35075  cvrnbtwn2  35231  cvrnbtwn3  35232  cvrnbtwn4  35235  cvlcvr1  35295  hlrelat2  35359  cvrat4  35399  islpln2a  35504  linepsubN  35708  elpaddn0  35756  paddssw2  35800  pmapjoin  35808  ispsubcl2N  35903  dochkrshp  37342  dochsatshp  37407  mapdh9a  37745  hdmap11lem2  37798  pwinfi3  38543  clsk1independent  39018  gneispace  39106  pm11.71  39271  sbgoldbaltlem2  42344  setrec1lem4  43106