Theorem jcad 522

Description: Deduction conjoining the consequents of two implications. Deduction form of jca 521 and double deduction form of pm3.2 475 and pm3.2i 476. (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 475	. 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃)))
4	1, 2, 3	syl6c 71	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jca2  523  jctild  535  jctird  536  ancld  560  ancrd  561  oplem1  1072  2eu1  2675  2eu1v  2676  disjxiun  5099  iss  6026  oneqmini  6416  funssres  6584  elpreima  7057  isomin  7345  oneqmin  7814  frxp  8140  soseq  8178  tposfo2  8269  oa00  8570  odi  8590  oneo  8592  oeordsuc  8606  oelim2  8607  nnarcl  8628  nnmord  8644  nnneo  8667  map0g  8915  pssnn  9187  fodomfib  9323  inf3lem4  9635  cplem1  9953  cplem1OLD  9954  kardenOLD  9963  setrec1lem4  9974  alephordi  10156  cardinfima  10179  dfac5lem5  10209  isf34lem4  10458  axcc4  10520  axdc3lem2  10532  zorn2lem4  10580  zorn2lem7  10583  indpi  10995  genpcl  11096  addclprlem2  11105  ltaddpr  11122  ltexprlem5  11128  suplem1pr  11140  ltlen  11414  dedekind  11476  sup2  12276  nominpos  12586  uzind  12794  xrmaxlt  13314  xrltmin  13315  xrmaxle  13316  xrlemin  13317  xmullem2  13398  ccatopth  14869  shftuz  15227  sqreulem  15532  limsupbnd2  15655  mulcn2  15768  sadcaddlem  16632  dvdsgcdb  16723  algcvgblem  16757  lcmdvdsb  16793  rpexp  16903  infpnlem1  17093  divsfval  17724  iscatd  17852  posasymb  18498  plttr  18519  joinle  18563  meetle  18577  latnlej  18635  latnlej2  18638  lsmlub  19883  imasring  20565  unitmulclb  20616  lbspss  21362  lspsneu  21406  lspprat  21436  assapropd  22184  isclo2  23411  cncls2  23596  cncls  23597  cnntr  23598  cnrest2  23609  cmpsub  23723  cmpcld  23725  kgenss  23867  ptpjpre1  23895  txlm  23972  qtoptop2  24023  cmphaushmeo  24124  fbun  24164  isfild  24182  fbasrn  24208  fgtr  24214  ufinffr  24253  rnelfm  24277  fmfnfmlem4  24281  ghmcnp  24439  metrest  24848  icoopnst  25265  iocopnst  25266  dvfsumlem2  26352  dgreq0  26589  plyexmo  26641  taylthlem2  26706  cxpeq0  27011  mumullem2  27512  chpchtsum  27551  bposlem7  27622  lgsqr  27683  ltsres  28024  nosupno  28065  noinfno  28080  ltlesnd  28137  uspgr2wlkeq  30231  subgrwlk  30274  wwlknllvtx  30440  ex-natded5.3-2  31014  ubthlem1  31477  axhcompl-zf  31605  ococss  31900  nmopun  32621  elpjrn  32797  stm1addi  32852  stm1add3i  32854  mdsl1i  32928  chrelat2i  32972  atexch  32988  atcvat4i  33004  mdsymlem3  33012  bnj600  35595  trssfir1om  35789  trssfir1omregs  35860  karddom  35885  kardsdom  35886  pthacycspth  35998  srepdflem1  36004  subfacval2  36038  climuzcnv  36522  3jcadALT  36538  fundmpss  36624  segconeq  36867  ifscgr  36901  endofsegid  36942  colinbtwnle  36975  trer  37196  ivthALT  37215  fnessref  37237  fnemeet2  37247  fnejoin2  37249  onsuct0  37321  bj-ideqg1  38178  bj-elid6  38184  bj-finsumval0  38299  bj-isrvec2  38314  bj-bary1  38326  icorempo  38367  isbasisrelowllem1  38371  isbasisrelowllem2  38372  relowlpssretop  38380  finxpsuclem  38413  poimirlem31  38662  isbnd2  38810  bfplem2  38850  ghomco  38918  cnf1dd  39115  contrd  39122  mpobi123f  39187  mptbi12f  39191  iss2  39369  refressn  39558  jca2r  40005  prter2  40031  lshpset2N  40269  cvrnbtwn2  40425  cvrnbtwn3  40426  cvrnbtwn4  40429  cvlcvr1  40489  hlrelat2  40553  cvrat4  40593  islpln2a  40698  linepsubN  40902  elpaddn0  40950  paddssw2  40994  pmapjoin  41002  ispsubcl2N  41097  dochkrshp  42536  dochsatshp  42601  mapdh9a  42939  hdmap11lem2  42992  sn-sup2  43648  frlmfzowrdb  43664  pwinfi3  44657  clsk1independent  45139  gneispace  45227  pm11.71  45474  relpmin  46035  ormkglobd  47980  2reu8i  48276  sbgoldbaltlem2  48971  oppcendc  50225