Theorem jcad 517

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  jca2  518  jctild  530  jctird  531  ancld  555  ancrd  556  oplem1  1062  2eu1  2655  2eu1v  2656  disjxiun  5076  iss  5994  oneqmini  6370  funssres  6536  elpreima  7006  isomin  7288  oneqmin  7750  frxp  8073  soseq  8106  tposfo2  8196  oa00  8491  odi  8511  oneo  8513  oeordsuc  8527  oelim2  8528  nnarcl  8549  nnmord  8565  nnneo  8588  map0g  8829  pssnn  9100  fodomfib  9236  fodomfibOLD  9238  inf3lem4  9550  cplem1  9811  karden  9817  alephordi  9994  cardinfima  10017  dfac5lem5  10047  isf34lem4  10297  axcc4  10359  axdc3lem2  10371  zorn2lem4  10419  zorn2lem7  10422  indpi  10828  genpcl  10929  addclprlem2  10938  ltaddpr  10955  ltexprlem5  10961  suplem1pr  10973  ltlen  11245  dedekind  11307  mulgt1OLD  12012  sup2  12110  nominpos  12412  uzind  12619  xrmaxlt  13131  xrltmin  13132  xrmaxle  13133  xrlemin  13134  xmullem2  13215  ccatopth  14676  shftuz  15029  sqreulem  15320  limsupbnd2  15443  mulcn2  15556  sadcaddlem  16424  dvdsgcdb  16512  algcvgblem  16544  lcmdvdsb  16580  rpexp  16690  infpnlem1  16879  divsfval  17509  iscatd  17637  posasymb  18283  plttr  18304  joinle  18348  meetle  18362  latnlej  18420  latnlej2  18423  lsmlub  19637  imasring  20308  unitmulclb  20359  lbspss  21079  lspsneu  21123  lspprat  21153  assapropd  21853  isclo2  23078  cncls2  23263  cncls  23264  cnntr  23265  cnrest2  23276  cmpsub  23390  cmpcld  23392  kgenss  23533  ptpjpre1  23561  txlm  23638  qtoptop2  23689  cmphaushmeo  23790  fbun  23830  isfild  23848  fbasrn  23874  fgtr  23880  ufinffr  23919  rnelfm  23943  fmfnfmlem4  23947  ghmcnp  24105  metrest  24514  icoopnst  24931  iocopnst  24932  dvfsumlem2  26019  dgreq0  26255  plyexmo  26304  taylthlem2  26364  cxpeq0  26667  mumullem2  27168  chpchtsum  27207  bposlem7  27278  lgsqr  27339  ltsres  27651  nosupno  27692  noinfno  27707  ltlesnd  27764  uspgr2wlkeq  29739  wwlknllvtx  29939  ex-natded5.3-2  30503  ubthlem1  30966  axhcompl-zf  31094  ococss  31389  nmopun  32110  elpjrn  32286  stm1addi  32341  stm1add3i  32343  mdsl1i  32417  chrelat2i  32461  atexch  32477  atcvat4i  32493  mdsymlem3  32501  bian1dOLD  32551  bnj600  35108  trssfir1om  35299  trssfir1omregs  35324  subgrwlk  35367  pthacycspth  35392  subfacval2  35422  climuzcnv  35906  3jcadALT  35922  fundmpss  36002  segconeq  36245  ifscgr  36279  endofsegid  36320  colinbtwnle  36353  trer  36551  ivthALT  36570  fnessref  36592  fnemeet2  36602  fnejoin2  36604  onsuct0  36676  bj-ideqg1  37531  bj-elid6  37537  bj-finsumval0  37652  bj-isrvec2  37667  bj-bary1  37679  icorempo  37720  isbasisrelowllem1  37724  isbasisrelowllem2  37725  relowlpssretop  37733  finxpsuclem  37766  pibt2  37786  poimirlem31  38025  isbnd2  38157  bfplem2  38197  ghomco  38265  cnf1dd  38464  contrd  38471  mpobi123f  38536  mptbi12f  38540  iss2  38718  refressn  38907  jca2r  39354  prter2  39380  lshpset2N  39618  cvrnbtwn2  39774  cvrnbtwn3  39775  cvrnbtwn4  39778  cvlcvr1  39838  hlrelat2  39902  cvrat4  39942  islpln2a  40047  linepsubN  40251  elpaddn0  40299  paddssw2  40343  pmapjoin  40351  ispsubcl2N  40446  dochkrshp  41885  dochsatshp  41950  mapdh9a  42288  hdmap11lem2  42341  sn-sup2  42988  frlmfzowrdb  43001  pwinfi3  44014  clsk1independent  44497  gneispace  44585  pm11.71  44848  relpmin  45403  ormkglobd  47327  2reu8i  47583  sbgoldbaltlem2  48278  oppcendc  49515  setrec1lem4  50187