Theorem jcad 555

Description: Deduction conjoining the consequents of two implications. (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 463	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 70	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  jca2  556  jctild  566  jctird  567  ancld  576  ancrd  577  anim12ii  594  oplem1  1007  2eu1  2553  rr19.28v  3346  disjxiun  4649  disjxiunOLD  4650  iss  5447  preddowncl  5707  oneqmini  5776  funssres  5930  ssimaex  6263  elpreima  6337  isomin  6587  oneqmin  7005  frxp  7287  tposfo2  7375  onfununi  7438  oaordex  7638  oa00  7639  odi  7659  oneo  7661  oeordsuc  7674  oelim2  7675  nnarcl  7696  nnmord  7712  nnneo  7731  map0g  7897  mapsn  7899  domtriord  8106  onomeneq  8150  pssnn  8178  findcard3  8203  unfilem1  8224  fodomfib  8240  inf0  8518  inf3lem3  8527  inf3lem4  8528  tcel  8621  cplem1  8752  karden  8758  fidomtri2  8820  alephordi  8897  cardinfima  8920  alephval3  8933  dfac5lem5  8950  isf34lem4  9199  axcc4  9261  axdc3lem2  9273  zorn2lem4  9321  zorn2lem6  9323  zorn2lem7  9324  fodomb  9348  indpi  9729  genpcl  9830  addclprlem2  9839  ltaddpr  9856  ltexprlem5  9862  suplem1pr  9874  ltlen  10138  dedekind  10200  mulgt1  10882  sup2  10979  nominpos  11269  uzind  11469  eqreznegel  11774  xrmaxlt  12012  xrltmin  12013  xrmaxle  12014  xrlemin  12015  xmullem2  12095  ccatopth  13470  shftuz  13809  sqreulem  14099  limsupbnd2  14214  mulcn2  14326  sadcaddlem  15179  dvdsgcdb  15262  algcvgblem  15290  lcmdvdsb  15326  rpexp  15432  iserodd  15540  infpnlem1  15614  divsfval  16207  iscatd  16334  posasymb  16952  plttr  16970  joinle  17014  meetle  17028  latnlej  17068  latnlej2  17071  lsmlub  18078  imasring  18619  unitmulclb  18665  lbspss  19082  lspsneu  19123  lspprat  19153  assapropd  19327  isclo2  20892  cncls2  21077  cncls  21078  cnntr  21079  cnrest2  21090  cmpsub  21203  cmpcld  21205  kgenss  21346  ptpjpre1  21374  txcn  21429  txlm  21451  qtoptop2  21502  cmphaushmeo  21603  fbun  21644  isfild  21662  ssfg  21676  fbasrn  21688  fgtr  21694  ufinffr  21733  rnelfm  21757  fmfnfmlem4  21761  fclsnei  21823  ghmcnp  21918  metrest  22329  icoopnst  22738  iocopnst  22739  dgreq0  24021  plyexmo  24068  cxpeq0  24424  eldmgm  24748  mumullem2  24906  chpchtsum  24944  bposlem7  25015  lgsqr  25076  uspgr2wlkeq  26542  ex-natded5.3-2  27265  ubthlem1  27726  axhcompl-zf  27855  ococss  28152  nmopun  28873  elpjrn  29049  stm1addi  29104  stm1add3i  29106  mdsl1i  29180  chrelat2i  29224  atexch  29240  atcvat4i  29256  mdsymlem3  29264  bian1d  29306  bnj600  30989  subfacval2  31169  climuzcnv  31565  fundmpss  31664  soseq  31751  sltres  31815  nosupno  31849  segconeq  32117  ifscgr  32151  endofsegid  32192  colinbtwnle  32225  trer  32310  ivthALT  32330  fnessref  32352  fnemeet2  32362  fnejoin2  32364  onsuct0  32440  bj-finsumval0  33147  bj-bary1  33162  icorempt2  33199  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlpssretop  33212  finxpsuclem  33234  poimirlem31  33440  isbnd2  33582  bfplem2  33622  ghomco  33690  cnf1dd  33892  contrd  33899  mpt2bi123f  33971  mptbi12f  33975  iss2  34112  jca2r  34139  prter2  34166  lshpset2N  34406  cvrnbtwn2  34562  cvrnbtwn3  34563  cvrnbtwn4  34566  cvlcvr1  34626  hlrelat2  34689  cvrat4  34729  islpln2a  34834  linepsubN  35038  elpaddn0  35086  paddssw2  35130  pmapjoin  35138  ispsubcl2N  35233  dochkrshp  36675  dochsatshp  36740  mapdh9a  37079  hdmap11lem2  37134  pwinfi3  37868  rfovcnvf1od  38298  clsk1independent  38344  gneispace  38432  pm11.71  38597  sbgoldbaltlem2  41668  setrec1lem4  42437