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  1053  2eu1  2644  2eu1v  2645  disjxiun  5146  iss  6036  oneqmini  6417  funssres  6593  elpreima  7060  isomin  7338  oneqmin  7792  frxp  8116  soseq  8149  tposfo2  8238  oa00  8563  odi  8583  oneo  8585  oeordsuc  8598  oelim2  8599  nnarcl  8620  nnmord  8636  nnneo  8658  map0g  8882  pssnn  9172  onomeneqOLD  9233  pssnnOLD  9269  fodomfib  9330  inf3lem4  9630  cplem1  9888  karden  9894  alephordi  10073  cardinfima  10096  dfac5lem5  10126  isf34lem4  10376  axcc4  10438  axdc3lem2  10450  zorn2lem4  10498  zorn2lem7  10501  indpi  10906  genpcl  11007  addclprlem2  11016  ltaddpr  11033  ltexprlem5  11039  suplem1pr  11051  ltlen  11321  dedekind  11383  mulgt1  12079  sup2  12176  nominpos  12455  uzind  12660  xrmaxlt  13166  xrltmin  13167  xrmaxle  13168  xrlemin  13169  xmullem2  13250  ccatopth  14672  shftuz  15022  sqreulem  15312  limsupbnd2  15433  mulcn2  15546  sadcaddlem  16404  dvdsgcdb  16493  algcvgblem  16520  lcmdvdsb  16556  rpexp  16665  infpnlem1  16849  divsfval  17499  iscatd  17623  posasymb  18278  plttr  18301  joinle  18345  meetle  18359  latnlej  18415  latnlej2  18418  lsmlub  19575  imasring  20220  unitmulclb  20274  lbspss  20839  lspsneu  20883  lspprat  20913  assapropd  21647  isclo2  22814  cncls2  22999  cncls  23000  cnntr  23001  cnrest2  23012  cmpsub  23126  cmpcld  23128  kgenss  23269  ptpjpre1  23297  txlm  23374  qtoptop2  23425  cmphaushmeo  23526  fbun  23566  isfild  23584  fbasrn  23610  fgtr  23616  ufinffr  23655  rnelfm  23679  fmfnfmlem4  23683  ghmcnp  23841  metrest  24255  icoopnst  24685  iocopnst  24686  dgreq0  26013  plyexmo  26060  cxpeq0  26420  mumullem2  26918  chpchtsum  26956  bposlem7  27027  lgsqr  27088  sltres  27399  nosupno  27440  noinfno  27455  uspgr2wlkeq  29168  wwlknllvtx  29365  ex-natded5.3-2  29926  ubthlem1  30388  axhcompl-zf  30516  ococss  30811  nmopun  31532  elpjrn  31708  stm1addi  31763  stm1add3i  31765  mdsl1i  31839  chrelat2i  31883  atexch  31899  atcvat4i  31915  mdsymlem3  31923  bian1d  31965  bnj600  34226  subgrwlk  34419  pthacycspth  34444  subfacval2  34474  climuzcnv  34952  fundmpss  35040  segconeq  35284  ifscgr  35318  endofsegid  35359  colinbtwnle  35392  gg-dvfsumlem2  35471  trer  35506  ivthALT  35525  fnessref  35547  fnemeet2  35557  fnejoin2  35559  onsuct0  35631  bj-ideqg1  36350  bj-elid6  36356  bj-finsumval0  36471  bj-isrvec2  36486  bj-bary1  36498  icorempo  36537  isbasisrelowllem1  36541  isbasisrelowllem2  36542  relowlpssretop  36550  finxpsuclem  36583  pibt2  36603  poimirlem31  36824  isbnd2  36956  bfplem2  36996  ghomco  37064  cnf1dd  37263  contrd  37270  mpobi123f  37335  mptbi12f  37339  iss2  37518  refressn  37618  jca2r  38030  prter2  38056  lshpset2N  38294  cvrnbtwn2  38450  cvrnbtwn3  38451  cvrnbtwn4  38454  cvlcvr1  38514  hlrelat2  38579  cvrat4  38619  islpln2a  38724  linepsubN  38928  elpaddn0  38976  paddssw2  39020  pmapjoin  39028  ispsubcl2N  39123  dochkrshp  40562  dochsatshp  40627  mapdh9a  40965  hdmap11lem2  41018  frlmfzowrdb  41386  sn-sup2  41646  pwinfi3  42618  clsk1independent  43101  gneispace  43189  pm11.71  43460  tworepnotupword  45900  2reu8i  46121  sbgoldbaltlem2  46748  setrec1lem4  47824