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  2654  2eu1v  2655  disjxiun  5163  iss  6064  oneqmini  6447  funssres  6622  elpreima  7091  isomin  7373  oneqmin  7836  frxp  8167  soseq  8200  tposfo2  8290  oa00  8615  odi  8635  oneo  8637  oeordsuc  8650  oelim2  8651  nnarcl  8672  nnmord  8688  nnneo  8711  map0g  8942  pssnn  9234  onomeneqOLD  9292  fodomfib  9397  fodomfibOLD  9399  inf3lem4  9700  cplem1  9958  karden  9964  alephordi  10143  cardinfima  10166  dfac5lem5  10196  isf34lem4  10446  axcc4  10508  axdc3lem2  10520  zorn2lem4  10568  zorn2lem7  10571  indpi  10976  genpcl  11077  addclprlem2  11086  ltaddpr  11103  ltexprlem5  11109  suplem1pr  11121  ltlen  11391  dedekind  11453  mulgt1OLD  12153  sup2  12251  nominpos  12530  uzind  12735  xrmaxlt  13243  xrltmin  13244  xrmaxle  13245  xrlemin  13246  xmullem2  13327  ccatopth  14764  shftuz  15118  sqreulem  15408  limsupbnd2  15529  mulcn2  15642  sadcaddlem  16503  dvdsgcdb  16592  algcvgblem  16624  lcmdvdsb  16660  rpexp  16769  infpnlem1  16957  divsfval  17607  iscatd  17731  posasymb  18389  plttr  18412  joinle  18456  meetle  18470  latnlej  18526  latnlej2  18529  lsmlub  19706  imasring  20353  unitmulclb  20407  lbspss  21104  lspsneu  21148  lspprat  21178  assapropd  21915  isclo2  23117  cncls2  23302  cncls  23303  cnntr  23304  cnrest2  23315  cmpsub  23429  cmpcld  23431  kgenss  23572  ptpjpre1  23600  txlm  23677  qtoptop2  23728  cmphaushmeo  23829  fbun  23869  isfild  23887  fbasrn  23913  fgtr  23919  ufinffr  23958  rnelfm  23982  fmfnfmlem4  23986  ghmcnp  24144  metrest  24558  icoopnst  24988  iocopnst  24989  dvfsumlem2  26087  dgreq0  26325  plyexmo  26373  taylthlem2  26434  cxpeq0  26738  mumullem2  27241  chpchtsum  27281  bposlem7  27352  lgsqr  27413  sltres  27725  nosupno  27766  noinfno  27781  sltlend  27834  uspgr2wlkeq  29682  wwlknllvtx  29879  ex-natded5.3-2  30440  ubthlem1  30902  axhcompl-zf  31030  ococss  31325  nmopun  32046  elpjrn  32222  stm1addi  32277  stm1add3i  32279  mdsl1i  32353  chrelat2i  32397  atexch  32413  atcvat4i  32429  mdsymlem3  32437  bian1dOLD  32485  bnj600  34895  subgrwlk  35100  pthacycspth  35125  subfacval2  35155  climuzcnv  35639  3jcadALT  35655  fundmpss  35730  segconeq  35974  ifscgr  36008  endofsegid  36049  colinbtwnle  36082  trer  36282  ivthALT  36301  fnessref  36323  fnemeet2  36333  fnejoin2  36335  onsuct0  36407  bj-ideqg1  37130  bj-elid6  37136  bj-finsumval0  37251  bj-isrvec2  37266  bj-bary1  37278  icorempo  37317  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlpssretop  37330  finxpsuclem  37363  pibt2  37383  poimirlem31  37611  isbnd2  37743  bfplem2  37783  ghomco  37851  cnf1dd  38050  contrd  38057  mpobi123f  38122  mptbi12f  38126  iss2  38300  refressn  38399  jca2r  38811  prter2  38837  lshpset2N  39075  cvrnbtwn2  39231  cvrnbtwn3  39232  cvrnbtwn4  39235  cvlcvr1  39295  hlrelat2  39360  cvrat4  39400  islpln2a  39505  linepsubN  39709  elpaddn0  39757  paddssw2  39801  pmapjoin  39809  ispsubcl2N  39904  dochkrshp  41343  dochsatshp  41408  mapdh9a  41746  hdmap11lem2  41799  sn-sup2  42447  frlmfzowrdb  42459  pwinfi3  43525  clsk1independent  44008  gneispace  44096  pm11.71  44366  tworepnotupword  46805  2reu8i  47028  sbgoldbaltlem2  47654  setrec1lem4  48782