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  1057  2eu1  2651  2eu1v  2652  disjxiun  5140  iss  6053  oneqmini  6436  funssres  6610  elpreima  7078  isomin  7357  oneqmin  7820  frxp  8151  soseq  8184  tposfo2  8274  oa00  8597  odi  8617  oneo  8619  oeordsuc  8632  oelim2  8633  nnarcl  8654  nnmord  8670  nnneo  8693  map0g  8924  pssnn  9208  onomeneqOLD  9266  fodomfib  9369  fodomfibOLD  9371  inf3lem4  9671  cplem1  9929  karden  9935  alephordi  10114  cardinfima  10137  dfac5lem5  10167  isf34lem4  10417  axcc4  10479  axdc3lem2  10491  zorn2lem4  10539  zorn2lem7  10542  indpi  10947  genpcl  11048  addclprlem2  11057  ltaddpr  11074  ltexprlem5  11080  suplem1pr  11092  ltlen  11362  dedekind  11424  mulgt1OLD  12126  sup2  12224  nominpos  12503  uzind  12710  xrmaxlt  13223  xrltmin  13224  xrmaxle  13225  xrlemin  13226  xmullem2  13307  ccatopth  14754  shftuz  15108  sqreulem  15398  limsupbnd2  15519  mulcn2  15632  sadcaddlem  16494  dvdsgcdb  16582  algcvgblem  16614  lcmdvdsb  16650  rpexp  16759  infpnlem1  16948  divsfval  17592  iscatd  17716  posasymb  18365  plttr  18387  joinle  18431  meetle  18445  latnlej  18501  latnlej2  18504  lsmlub  19682  imasring  20327  unitmulclb  20381  lbspss  21081  lspsneu  21125  lspprat  21155  assapropd  21892  isclo2  23096  cncls2  23281  cncls  23282  cnntr  23283  cnrest2  23294  cmpsub  23408  cmpcld  23410  kgenss  23551  ptpjpre1  23579  txlm  23656  qtoptop2  23707  cmphaushmeo  23808  fbun  23848  isfild  23866  fbasrn  23892  fgtr  23898  ufinffr  23937  rnelfm  23961  fmfnfmlem4  23965  ghmcnp  24123  metrest  24537  icoopnst  24969  iocopnst  24970  dvfsumlem2  26067  dgreq0  26305  plyexmo  26355  taylthlem2  26416  cxpeq0  26720  mumullem2  27223  chpchtsum  27263  bposlem7  27334  lgsqr  27395  sltres  27707  nosupno  27748  noinfno  27763  sltlend  27816  uspgr2wlkeq  29664  wwlknllvtx  29866  ex-natded5.3-2  30427  ubthlem1  30889  axhcompl-zf  31017  ococss  31312  nmopun  32033  elpjrn  32209  stm1addi  32264  stm1add3i  32266  mdsl1i  32340  chrelat2i  32384  atexch  32400  atcvat4i  32416  mdsymlem3  32424  bian1dOLD  32476  bnj600  34933  subgrwlk  35137  pthacycspth  35162  subfacval2  35192  climuzcnv  35676  3jcadALT  35692  fundmpss  35767  segconeq  36011  ifscgr  36045  endofsegid  36086  colinbtwnle  36119  trer  36317  ivthALT  36336  fnessref  36358  fnemeet2  36368  fnejoin2  36370  onsuct0  36442  bj-ideqg1  37165  bj-elid6  37171  bj-finsumval0  37286  bj-isrvec2  37301  bj-bary1  37313  icorempo  37352  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlpssretop  37365  finxpsuclem  37398  pibt2  37418  poimirlem31  37658  isbnd2  37790  bfplem2  37830  ghomco  37898  cnf1dd  38097  contrd  38104  mpobi123f  38169  mptbi12f  38173  iss2  38345  refressn  38444  jca2r  38856  prter2  38882  lshpset2N  39120  cvrnbtwn2  39276  cvrnbtwn3  39277  cvrnbtwn4  39280  cvlcvr1  39340  hlrelat2  39405  cvrat4  39445  islpln2a  39550  linepsubN  39754  elpaddn0  39802  paddssw2  39846  pmapjoin  39854  ispsubcl2N  39949  dochkrshp  41388  dochsatshp  41453  mapdh9a  41791  hdmap11lem2  41844  sn-sup2  42501  frlmfzowrdb  42514  pwinfi3  43576  clsk1independent  44059  gneispace  44147  pm11.71  44416  relpmin  44973  ormkglobd  46890  tworepnotupword  46901  2reu8i  47125  sbgoldbaltlem2  47767  oppcendc  48906  setrec1lem4  49209