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  2648  2eu1v  2649  disjxiun  5090  iss  5988  oneqmini  6364  funssres  6530  elpreima  6997  isomin  7277  oneqmin  7739  frxp  8062  soseq  8095  tposfo2  8185  oa00  8480  odi  8500  oneo  8502  oeordsuc  8515  oelim2  8516  nnarcl  8537  nnmord  8553  nnneo  8576  map0g  8814  pssnn  9085  fodomfib  9220  fodomfibOLD  9222  inf3lem4  9528  cplem1  9789  karden  9795  alephordi  9972  cardinfima  9995  dfac5lem5  10025  isf34lem4  10275  axcc4  10337  axdc3lem2  10349  zorn2lem4  10397  zorn2lem7  10400  indpi  10805  genpcl  10906  addclprlem2  10915  ltaddpr  10932  ltexprlem5  10938  suplem1pr  10950  ltlen  11221  dedekind  11283  mulgt1OLD  11987  sup2  12085  nominpos  12365  uzind  12571  xrmaxlt  13082  xrltmin  13083  xrmaxle  13084  xrlemin  13085  xmullem2  13166  ccatopth  14625  shftuz  14978  sqreulem  15269  limsupbnd2  15392  mulcn2  15505  sadcaddlem  16370  dvdsgcdb  16458  algcvgblem  16490  lcmdvdsb  16526  rpexp  16635  infpnlem1  16824  divsfval  17453  iscatd  17581  posasymb  18227  plttr  18248  joinle  18292  meetle  18306  latnlej  18364  latnlej2  18367  lsmlub  19578  imasring  20250  unitmulclb  20301  lbspss  21018  lspsneu  21062  lspprat  21092  assapropd  21811  isclo2  23004  cncls2  23189  cncls  23190  cnntr  23191  cnrest2  23202  cmpsub  23316  cmpcld  23318  kgenss  23459  ptpjpre1  23487  txlm  23564  qtoptop2  23615  cmphaushmeo  23716  fbun  23756  isfild  23774  fbasrn  23800  fgtr  23806  ufinffr  23845  rnelfm  23869  fmfnfmlem4  23873  ghmcnp  24031  metrest  24440  icoopnst  24864  iocopnst  24865  dvfsumlem2  25961  dgreq0  26199  plyexmo  26249  taylthlem2  26310  cxpeq0  26615  mumullem2  27118  chpchtsum  27158  bposlem7  27229  lgsqr  27290  sltres  27602  nosupno  27643  noinfno  27658  sltlend  27711  uspgr2wlkeq  29626  wwlknllvtx  29826  ex-natded5.3-2  30390  ubthlem1  30852  axhcompl-zf  30980  ococss  31275  nmopun  31996  elpjrn  32172  stm1addi  32227  stm1add3i  32229  mdsl1i  32303  chrelat2i  32347  atexch  32363  atcvat4i  32379  mdsymlem3  32387  bian1dOLD  32438  bnj600  34952  trssfir1om  35143  trssfir1omregs  35153  subgrwlk  35197  pthacycspth  35222  subfacval2  35252  climuzcnv  35736  3jcadALT  35752  fundmpss  35832  segconeq  36075  ifscgr  36109  endofsegid  36150  colinbtwnle  36183  trer  36381  ivthALT  36400  fnessref  36422  fnemeet2  36432  fnejoin2  36434  onsuct0  36506  bj-ideqg1  37229  bj-elid6  37235  bj-finsumval0  37350  bj-isrvec2  37365  bj-bary1  37377  icorempo  37416  isbasisrelowllem1  37420  isbasisrelowllem2  37421  relowlpssretop  37429  finxpsuclem  37462  pibt2  37482  poimirlem31  37711  isbnd2  37843  bfplem2  37883  ghomco  37951  cnf1dd  38150  contrd  38157  mpobi123f  38222  mptbi12f  38226  iss2  38396  refressn  38565  jca2r  38974  prter2  39000  lshpset2N  39238  cvrnbtwn2  39394  cvrnbtwn3  39395  cvrnbtwn4  39398  cvlcvr1  39458  hlrelat2  39522  cvrat4  39562  islpln2a  39667  linepsubN  39871  elpaddn0  39919  paddssw2  39963  pmapjoin  39971  ispsubcl2N  40066  dochkrshp  41505  dochsatshp  41570  mapdh9a  41908  hdmap11lem2  41961  sn-sup2  42609  frlmfzowrdb  42622  pwinfi3  43680  clsk1independent  44163  gneispace  44251  pm11.71  44514  relpmin  45069  ormkglobd  46997  2reu8i  47237  sbgoldbaltlem2  47904  oppcendc  49143  setrec1lem4  49815