Theorem jcad 520

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  jca2  521  jctild  533  jctird  534  ancld  558  ancrd  559  oplem1  1067  2eu1  2676  2eu1v  2677  disjxiun  5096  iss  6021  oneqmini  6395  funssres  6561  elpreima  7035  isomin  7317  oneqmin  7779  frxp  8101  soseq  8134  tposfo2  8224  oa00  8523  odi  8543  oneo  8545  oeordsuc  8559  oelim2  8560  nnarcl  8581  nnmord  8597  nnneo  8620  map0g  8862  pssnn  9133  fodomfib  9269  fodomfibOLD  9271  inf3lem4  9583  cplem1  9844  karden  9850  alephordi  10027  cardinfima  10050  dfac5lem5  10080  isf34lem4  10331  axcc4  10393  axdc3lem2  10405  zorn2lem4  10453  zorn2lem7  10456  indpi  10862  genpcl  10963  addclprlem2  10972  ltaddpr  10989  ltexprlem5  10995  suplem1pr  11007  ltlen  11281  dedekind  11343  mulgt1OLD  12047  sup2  12145  nominpos  12455  uzind  12662  xrmaxlt  13181  xrltmin  13182  xrmaxle  13183  xrlemin  13184  xmullem2  13265  ccatopth  14726  shftuz  15079  sqreulem  15370  limsupbnd2  15493  mulcn2  15606  sadcaddlem  16474  dvdsgcdb  16562  algcvgblem  16594  lcmdvdsb  16630  rpexp  16740  infpnlem1  16929  divsfval  17560  iscatd  17688  posasymb  18334  plttr  18355  joinle  18399  meetle  18413  latnlej  18471  latnlej2  18474  lsmlub  19687  imasring  20358  unitmulclb  20409  lbspss  21129  lspsneu  21173  lspprat  21203  assapropd  21903  isclo2  23128  cncls2  23313  cncls  23314  cnntr  23315  cnrest2  23326  cmpsub  23440  cmpcld  23442  kgenss  23583  ptpjpre1  23611  txlm  23688  qtoptop2  23739  cmphaushmeo  23840  fbun  23880  isfild  23898  fbasrn  23924  fgtr  23930  ufinffr  23969  rnelfm  23993  fmfnfmlem4  23997  ghmcnp  24155  metrest  24564  icoopnst  24981  iocopnst  24982  dvfsumlem2  26069  dgreq0  26305  plyexmo  26354  taylthlem2  26414  cxpeq0  26720  mumullem2  27221  chpchtsum  27260  bposlem7  27331  lgsqr  27392  ltsres  27703  nosupno  27744  noinfno  27759  ltlesnd  27816  uspgr2wlkeq  29792  wwlknllvtx  29992  ex-natded5.3-2  30556  ubthlem1  31019  axhcompl-zf  31147  ococss  31442  nmopun  32163  elpjrn  32339  stm1addi  32394  stm1add3i  32396  mdsl1i  32470  chrelat2i  32514  atexch  32530  atcvat4i  32546  mdsymlem3  32554  bian1dOLD  32604  bnj600  35178  trssfir1om  35371  trssfir1omregs  35396  subgrwlk  35446  pthacycspth  35471  subfacval2  35501  climuzcnv  35985  3jcadALT  36001  fundmpss  36081  segconeq  36324  ifscgr  36358  endofsegid  36399  colinbtwnle  36432  trer  36640  ivthALT  36659  fnessref  36681  fnemeet2  36691  fnejoin2  36693  onsuct0  36765  bj-ideqg1  37620  bj-elid6  37626  bj-finsumval0  37741  bj-isrvec2  37756  bj-bary1  37768  icorempo  37809  isbasisrelowllem1  37813  isbasisrelowllem2  37814  relowlpssretop  37822  finxpsuclem  37855  pibt2  37875  poimirlem31  38114  isbnd2  38246  bfplem2  38286  ghomco  38354  cnf1dd  38553  contrd  38560  mpobi123f  38625  mptbi12f  38629  iss2  38807  refressn  38996  jca2r  39443  prter2  39469  lshpset2N  39707  cvrnbtwn2  39863  cvrnbtwn3  39864  cvrnbtwn4  39867  cvlcvr1  39927  hlrelat2  39991  cvrat4  40031  islpln2a  40136  linepsubN  40340  elpaddn0  40388  paddssw2  40432  pmapjoin  40440  ispsubcl2N  40535  dochkrshp  41974  dochsatshp  42039  mapdh9a  42377  hdmap11lem2  42430  sn-sup2  43077  frlmfzowrdb  43090  pwinfi3  44103  clsk1independent  44586  gneispace  44674  pm11.71  44937  relpmin  45492  ormkglobd  47415  2reu8i  47671  sbgoldbaltlem2  48366  oppcendc  49603  setrec1lem4  50275