Theorem jcad 511

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  jca2  512  jctild  524  jctird  525  ancld  549  ancrd  550  oplem1  1054  2eu1  2639  2eu1v  2640  disjxiun  5146  iss  6040  oneqmini  6423  funssres  6598  elpreima  7066  isomin  7344  oneqmin  7804  frxp  8131  soseq  8164  tposfo2  8255  oa00  8580  odi  8600  oneo  8602  oeordsuc  8615  oelim2  8616  nnarcl  8637  nnmord  8653  nnneo  8676  map0g  8903  pssnn  9196  onomeneqOLD  9257  pssnnOLD  9293  fodomfib  9357  inf3lem4  9661  cplem1  9919  karden  9925  alephordi  10104  cardinfima  10127  dfac5lem5  10157  isf34lem4  10407  axcc4  10469  axdc3lem2  10481  zorn2lem4  10529  zorn2lem7  10532  indpi  10937  genpcl  11038  addclprlem2  11047  ltaddpr  11064  ltexprlem5  11070  suplem1pr  11082  ltlen  11352  dedekind  11414  mulgt1  12111  sup2  12208  nominpos  12487  uzind  12692  xrmaxlt  13200  xrltmin  13201  xrmaxle  13202  xrlemin  13203  xmullem2  13284  ccatopth  14707  shftuz  15057  sqreulem  15347  limsupbnd2  15468  mulcn2  15581  sadcaddlem  16440  dvdsgcdb  16529  algcvgblem  16556  lcmdvdsb  16592  rpexp  16702  infpnlem1  16887  divsfval  17537  iscatd  17661  posasymb  18319  plttr  18342  joinle  18386  meetle  18400  latnlej  18456  latnlej2  18459  lsmlub  19636  imasring  20283  unitmulclb  20337  lbspss  20984  lspsneu  21028  lspprat  21058  assapropd  21827  isclo2  23041  cncls2  23226  cncls  23227  cnntr  23228  cnrest2  23239  cmpsub  23353  cmpcld  23355  kgenss  23496  ptpjpre1  23524  txlm  23601  qtoptop2  23652  cmphaushmeo  23753  fbun  23793  isfild  23811  fbasrn  23837  fgtr  23843  ufinffr  23882  rnelfm  23906  fmfnfmlem4  23910  ghmcnp  24068  metrest  24482  icoopnst  24912  iocopnst  24913  dvfsumlem2  26010  dgreq0  26250  plyexmo  26298  taylthlem2  26359  cxpeq0  26662  mumullem2  27162  chpchtsum  27202  bposlem7  27273  lgsqr  27334  sltres  27646  nosupno  27687  noinfno  27702  sltlend  27755  uspgr2wlkeq  29537  wwlknllvtx  29734  ex-natded5.3-2  30295  ubthlem1  30757  axhcompl-zf  30885  ococss  31180  nmopun  31901  elpjrn  32077  stm1addi  32132  stm1add3i  32134  mdsl1i  32208  chrelat2i  32252  atexch  32268  atcvat4i  32284  mdsymlem3  32292  bian1d  32339  bnj600  34683  subgrwlk  34875  pthacycspth  34900  subfacval2  34930  climuzcnv  35408  fundmpss  35495  segconeq  35739  ifscgr  35773  endofsegid  35814  colinbtwnle  35847  trer  35933  ivthALT  35952  fnessref  35974  fnemeet2  35984  fnejoin2  35986  onsuct0  36058  bj-ideqg1  36776  bj-elid6  36782  bj-finsumval0  36897  bj-isrvec2  36912  bj-bary1  36924  icorempo  36963  isbasisrelowllem1  36967  isbasisrelowllem2  36968  relowlpssretop  36976  finxpsuclem  37009  pibt2  37029  poimirlem31  37257  isbnd2  37389  bfplem2  37429  ghomco  37497  cnf1dd  37696  contrd  37703  mpobi123f  37768  mptbi12f  37772  iss2  37948  refressn  38047  jca2r  38459  prter2  38485  lshpset2N  38723  cvrnbtwn2  38879  cvrnbtwn3  38880  cvrnbtwn4  38883  cvlcvr1  38943  hlrelat2  39008  cvrat4  39048  islpln2a  39153  linepsubN  39357  elpaddn0  39405  paddssw2  39449  pmapjoin  39457  ispsubcl2N  39552  dochkrshp  40991  dochsatshp  41056  mapdh9a  41394  hdmap11lem2  41447  frlmfzowrdb  41884  sn-sup2  42161  pwinfi3  43137  clsk1independent  43620  gneispace  43708  pm11.71  43978  tworepnotupword  46412  2reu8i  46633  sbgoldbaltlem2  47259  setrec1lem4  48309