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  2651  2eu1v  2652  disjxiun  5095  iss  5994  oneqmini  6370  funssres  6536  elpreima  7003  isomin  7283  oneqmin  7745  frxp  8068  soseq  8101  tposfo2  8191  oa00  8486  odi  8506  oneo  8508  oeordsuc  8522  oelim2  8523  nnarcl  8544  nnmord  8560  nnneo  8583  map0g  8822  pssnn  9093  fodomfib  9229  fodomfibOLD  9231  inf3lem4  9540  cplem1  9801  karden  9807  alephordi  9984  cardinfima  10007  dfac5lem5  10037  isf34lem4  10287  axcc4  10349  axdc3lem2  10361  zorn2lem4  10409  zorn2lem7  10412  indpi  10818  genpcl  10919  addclprlem2  10928  ltaddpr  10945  ltexprlem5  10951  suplem1pr  10963  ltlen  11234  dedekind  11296  mulgt1OLD  12000  sup2  12098  nominpos  12378  uzind  12584  xrmaxlt  13096  xrltmin  13097  xrmaxle  13098  xrlemin  13099  xmullem2  13180  ccatopth  14639  shftuz  14992  sqreulem  15283  limsupbnd2  15406  mulcn2  15519  sadcaddlem  16384  dvdsgcdb  16472  algcvgblem  16504  lcmdvdsb  16540  rpexp  16649  infpnlem1  16838  divsfval  17468  iscatd  17596  posasymb  18242  plttr  18263  joinle  18307  meetle  18321  latnlej  18379  latnlej2  18382  lsmlub  19593  imasring  20266  unitmulclb  20317  lbspss  21034  lspsneu  21078  lspprat  21108  assapropd  21827  isclo2  23032  cncls2  23217  cncls  23218  cnntr  23219  cnrest2  23230  cmpsub  23344  cmpcld  23346  kgenss  23487  ptpjpre1  23515  txlm  23592  qtoptop2  23643  cmphaushmeo  23744  fbun  23784  isfild  23802  fbasrn  23828  fgtr  23834  ufinffr  23873  rnelfm  23897  fmfnfmlem4  23901  ghmcnp  24059  metrest  24468  icoopnst  24892  iocopnst  24893  dvfsumlem2  25989  dgreq0  26227  plyexmo  26277  taylthlem2  26338  cxpeq0  26643  mumullem2  27146  chpchtsum  27186  bposlem7  27257  lgsqr  27318  ltsres  27630  nosupno  27671  noinfno  27686  ltlesnd  27743  uspgr2wlkeq  29719  wwlknllvtx  29919  ex-natded5.3-2  30483  ubthlem1  30945  axhcompl-zf  31073  ococss  31368  nmopun  32089  elpjrn  32265  stm1addi  32320  stm1add3i  32322  mdsl1i  32396  chrelat2i  32440  atexch  32456  atcvat4i  32472  mdsymlem3  32480  bian1dOLD  32531  bnj600  35075  trssfir1om  35267  trssfir1omregs  35292  subgrwlk  35326  pthacycspth  35351  subfacval2  35381  climuzcnv  35865  3jcadALT  35881  fundmpss  35961  segconeq  36204  ifscgr  36238  endofsegid  36279  colinbtwnle  36312  trer  36510  ivthALT  36529  fnessref  36551  fnemeet2  36561  fnejoin2  36563  onsuct0  36635  bj-ideqg1  37365  bj-elid6  37371  bj-finsumval0  37486  bj-isrvec2  37501  bj-bary1  37513  icorempo  37552  isbasisrelowllem1  37556  isbasisrelowllem2  37557  relowlpssretop  37565  finxpsuclem  37598  pibt2  37618  poimirlem31  37848  isbnd2  37980  bfplem2  38020  ghomco  38088  cnf1dd  38287  contrd  38294  mpobi123f  38359  mptbi12f  38363  iss2  38533  refressn  38702  jca2r  39111  prter2  39137  lshpset2N  39375  cvrnbtwn2  39531  cvrnbtwn3  39532  cvrnbtwn4  39535  cvlcvr1  39595  hlrelat2  39659  cvrat4  39699  islpln2a  39804  linepsubN  40008  elpaddn0  40056  paddssw2  40100  pmapjoin  40108  ispsubcl2N  40203  dochkrshp  41642  dochsatshp  41707  mapdh9a  42045  hdmap11lem2  42098  sn-sup2  42742  frlmfzowrdb  42755  pwinfi3  43800  clsk1independent  44283  gneispace  44371  pm11.71  44634  relpmin  45189  ormkglobd  47115  2reu8i  47355  sbgoldbaltlem2  48022  oppcendc  49259  setrec1lem4  49931