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 207  df-an 396

This theorem is referenced by:  jca2  513  jctild  525  jctird  526  ancld  550  ancrd  551  oplem1  1056  2eu1  2644  2eu1v  2645  disjxiun  5104  iss  6006  oneqmini  6385  funssres  6560  elpreima  7030  isomin  7312  oneqmin  7776  frxp  8105  soseq  8138  tposfo2  8228  oa00  8523  odi  8543  oneo  8545  oeordsuc  8558  oelim2  8559  nnarcl  8580  nnmord  8596  nnneo  8619  map0g  8857  pssnn  9132  fodomfib  9280  fodomfibOLD  9282  inf3lem4  9584  cplem1  9842  karden  9848  alephordi  10027  cardinfima  10050  dfac5lem5  10080  isf34lem4  10330  axcc4  10392  axdc3lem2  10404  zorn2lem4  10452  zorn2lem7  10455  indpi  10860  genpcl  10961  addclprlem2  10970  ltaddpr  10987  ltexprlem5  10993  suplem1pr  11005  ltlen  11275  dedekind  11337  mulgt1OLD  12041  sup2  12139  nominpos  12419  uzind  12626  xrmaxlt  13141  xrltmin  13142  xrmaxle  13143  xrlemin  13144  xmullem2  13225  ccatopth  14681  shftuz  15035  sqreulem  15326  limsupbnd2  15449  mulcn2  15562  sadcaddlem  16427  dvdsgcdb  16515  algcvgblem  16547  lcmdvdsb  16583  rpexp  16692  infpnlem1  16881  divsfval  17510  iscatd  17634  posasymb  18280  plttr  18301  joinle  18345  meetle  18359  latnlej  18415  latnlej2  18418  lsmlub  19594  imasring  20239  unitmulclb  20290  lbspss  20989  lspsneu  21033  lspprat  21063  assapropd  21781  isclo2  22975  cncls2  23160  cncls  23161  cnntr  23162  cnrest2  23173  cmpsub  23287  cmpcld  23289  kgenss  23430  ptpjpre1  23458  txlm  23535  qtoptop2  23586  cmphaushmeo  23687  fbun  23727  isfild  23745  fbasrn  23771  fgtr  23777  ufinffr  23816  rnelfm  23840  fmfnfmlem4  23844  ghmcnp  24002  metrest  24412  icoopnst  24836  iocopnst  24837  dvfsumlem2  25933  dgreq0  26171  plyexmo  26221  taylthlem2  26282  cxpeq0  26587  mumullem2  27090  chpchtsum  27130  bposlem7  27201  lgsqr  27262  sltres  27574  nosupno  27615  noinfno  27630  sltlend  27683  uspgr2wlkeq  29574  wwlknllvtx  29776  ex-natded5.3-2  30337  ubthlem1  30799  axhcompl-zf  30927  ococss  31222  nmopun  31943  elpjrn  32119  stm1addi  32174  stm1add3i  32176  mdsl1i  32250  chrelat2i  32294  atexch  32310  atcvat4i  32326  mdsymlem3  32334  bian1dOLD  32386  bnj600  34909  subgrwlk  35119  pthacycspth  35144  subfacval2  35174  climuzcnv  35658  3jcadALT  35674  fundmpss  35754  segconeq  35998  ifscgr  36032  endofsegid  36073  colinbtwnle  36106  trer  36304  ivthALT  36323  fnessref  36345  fnemeet2  36355  fnejoin2  36357  onsuct0  36429  bj-ideqg1  37152  bj-elid6  37158  bj-finsumval0  37273  bj-isrvec2  37288  bj-bary1  37300  icorempo  37339  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlpssretop  37352  finxpsuclem  37385  pibt2  37405  poimirlem31  37645  isbnd2  37777  bfplem2  37817  ghomco  37885  cnf1dd  38084  contrd  38091  mpobi123f  38156  mptbi12f  38160  iss2  38326  refressn  38434  jca2r  38848  prter2  38874  lshpset2N  39112  cvrnbtwn2  39268  cvrnbtwn3  39269  cvrnbtwn4  39272  cvlcvr1  39332  hlrelat2  39397  cvrat4  39437  islpln2a  39542  linepsubN  39746  elpaddn0  39794  paddssw2  39838  pmapjoin  39846  ispsubcl2N  39941  dochkrshp  41380  dochsatshp  41445  mapdh9a  41783  hdmap11lem2  41836  sn-sup2  42479  frlmfzowrdb  42492  pwinfi3  43552  clsk1independent  44035  gneispace  44123  pm11.71  44386  relpmin  44942  ormkglobd  46873  tworepnotupword  46884  2reu8i  47114  sbgoldbaltlem2  47781  oppcendc  49007  setrec1lem4  49679