Theorem jcad 512

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  jca2  513  jctild  525  jctird  526  ancld  550  ancrd  551  oplem1  1053  2eu1  2652  2eu1v  2653  disjxiun  5067  iss  5932  oneqmini  6302  funssres  6462  elpreima  6917  isomin  7188  oneqmin  7627  frxp  7938  tposfo2  8036  oa00  8352  odi  8372  oneo  8374  oeordsuc  8387  oelim2  8388  nnarcl  8409  nnmord  8425  nnneo  8445  map0g  8630  pssnn  8913  onomeneq  8943  pssnnOLD  8969  fodomfib  9023  inf3lem4  9319  cplem1  9578  karden  9584  alephordi  9761  cardinfima  9784  dfac5lem5  9814  isf34lem4  10064  axcc4  10126  axdc3lem2  10138  zorn2lem4  10186  zorn2lem7  10189  indpi  10594  genpcl  10695  addclprlem2  10704  ltaddpr  10721  ltexprlem5  10727  suplem1pr  10739  ltlen  11006  dedekind  11068  mulgt1  11764  sup2  11861  nominpos  12140  uzind  12342  xrmaxlt  12844  xrltmin  12845  xrmaxle  12846  xrlemin  12847  xmullem2  12928  ccatopth  14357  shftuz  14708  sqreulem  14999  limsupbnd2  15120  mulcn2  15233  sadcaddlem  16092  dvdsgcdb  16181  algcvgblem  16210  lcmdvdsb  16246  rpexp  16355  infpnlem1  16539  divsfval  17175  iscatd  17299  posasymb  17952  plttr  17975  joinle  18019  meetle  18033  latnlej  18089  latnlej2  18092  lsmlub  19185  imasring  19773  unitmulclb  19822  lbspss  20259  lspsneu  20300  lspprat  20330  assapropd  20986  isclo2  22147  cncls2  22332  cncls  22333  cnntr  22334  cnrest2  22345  cmpsub  22459  cmpcld  22461  kgenss  22602  ptpjpre1  22630  txlm  22707  qtoptop2  22758  cmphaushmeo  22859  fbun  22899  isfild  22917  fbasrn  22943  fgtr  22949  ufinffr  22988  rnelfm  23012  fmfnfmlem4  23016  ghmcnp  23174  metrest  23586  icoopnst  24008  iocopnst  24009  dgreq0  25331  plyexmo  25378  cxpeq0  25738  mumullem2  26234  chpchtsum  26272  bposlem7  26343  lgsqr  26404  uspgr2wlkeq  27915  wwlknllvtx  28112  ex-natded5.3-2  28673  ubthlem1  29133  axhcompl-zf  29261  ococss  29556  nmopun  30277  elpjrn  30453  stm1addi  30508  stm1add3i  30510  mdsl1i  30584  chrelat2i  30628  atexch  30644  atcvat4i  30660  mdsymlem3  30668  bian1d  30710  bnj600  32799  subgrwlk  32994  pthacycspth  33019  subfacval2  33049  climuzcnv  33529  fundmpss  33646  soseq  33730  sltres  33792  nosupno  33833  noinfno  33848  segconeq  34239  ifscgr  34273  endofsegid  34314  colinbtwnle  34347  trer  34432  ivthALT  34451  fnessref  34473  fnemeet2  34483  fnejoin2  34485  onsuct0  34557  bj-ideqg1  35262  bj-elid6  35268  bj-finsumval0  35383  bj-isrvec2  35398  bj-bary1  35410  icorempo  35449  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlpssretop  35462  finxpsuclem  35495  pibt2  35515  poimirlem31  35735  isbnd2  35868  bfplem2  35908  ghomco  35976  cnf1dd  36175  contrd  36182  mpobi123f  36247  mptbi12f  36251  iss2  36406  jca2r  36796  prter2  36822  lshpset2N  37060  cvrnbtwn2  37216  cvrnbtwn3  37217  cvrnbtwn4  37220  cvlcvr1  37280  hlrelat2  37344  cvrat4  37384  islpln2a  37489  linepsubN  37693  elpaddn0  37741  paddssw2  37785  pmapjoin  37793  ispsubcl2N  37888  dochkrshp  39327  dochsatshp  39392  mapdh9a  39730  hdmap11lem2  39783  frlmfzowrdb  40161  sn-sup2  40360  pwinfi3  41059  clsk1independent  41545  gneispace  41633  pm11.71  41904  2reu8i  44492  sbgoldbaltlem2  45120  setrec1lem4  46282