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  2681  2eu1v  2682  disjxiun  5111  iss  6042  oneqmini  6421  funssres  6587  elpreima  7060  isomin  7346  oneqmin  7808  frxp  8131  soseq  8164  tposfo2  8254  oa00  8553  odi  8573  oneo  8575  oeordsuc  8589  oelim2  8590  nnarcl  8611  nnmord  8627  nnneo  8650  map0g  8891  pssnn  9163  fodomfib  9298  inf3lem4  9610  cplem1  9889  cplem1OLD  9890  kardenOLD  9899  alephordi  10077  cardinfima  10100  dfac5lem5  10130  isf34lem4  10379  axcc4  10441  axdc3lem2  10453  zorn2lem4  10501  zorn2lem7  10504  indpi  10910  genpcl  11011  addclprlem2  11020  ltaddpr  11037  ltexprlem5  11043  suplem1pr  11055  ltlen  11329  dedekind  11391  sup2  12189  nominpos  12499  uzind  12706  xrmaxlt  13225  xrltmin  13226  xrmaxle  13227  xrlemin  13228  xmullem2  13309  ccatopth  14777  shftuz  15132  sqreulem  15437  limsupbnd2  15560  mulcn2  15673  sadcaddlem  16540  dvdsgcdb  16628  algcvgblem  16660  lcmdvdsb  16696  rpexp  16806  infpnlem1  16995  divsfval  17626  iscatd  17754  posasymb  18400  plttr  18421  joinle  18465  meetle  18479  latnlej  18537  latnlej2  18540  lsmlub  19765  imasring  20445  unitmulclb  20496  lbspss  21240  lspsneu  21284  lspprat  21314  assapropd  22058  isclo2  23282  cncls2  23467  cncls  23468  cnntr  23469  cnrest2  23480  cmpsub  23594  cmpcld  23596  kgenss  23737  ptpjpre1  23765  txlm  23842  qtoptop2  23893  cmphaushmeo  23994  fbun  24034  isfild  24052  fbasrn  24078  fgtr  24084  ufinffr  24123  rnelfm  24147  fmfnfmlem4  24151  ghmcnp  24309  metrest  24718  icoopnst  25135  iocopnst  25136  dvfsumlem2  26223  dgreq0  26459  plyexmo  26511  taylthlem2  26574  cxpeq0  26880  mumullem2  27381  chpchtsum  27420  bposlem7  27491  lgsqr  27552  ltsres  27863  nosupno  27904  noinfno  27919  ltlesnd  27976  uspgr2wlkeq  30032  wwlknllvtx  30232  ex-natded5.3-2  30796  ubthlem1  31259  axhcompl-zf  31387  ococss  31682  nmopun  32403  elpjrn  32579  stm1addi  32634  stm1add3i  32636  mdsl1i  32710  chrelat2i  32754  atexch  32770  atcvat4i  32786  mdsymlem3  32794  bnj600  35339  trssfir1om  35532  trssfir1omregs  35573  karddom  35598  kardsdom  35599  subgrwlk  35645  pthacycspth  35670  subfacval2  35700  climuzcnv  36184  3jcadALT  36200  fundmpss  36280  segconeq  36523  ifscgr  36557  endofsegid  36598  colinbtwnle  36631  trer  36868  ivthALT  36887  fnessref  36909  fnemeet2  36919  fnejoin2  36921  onsuct0  36993  bj-ideqg1  37849  bj-elid6  37855  bj-finsumval0  37970  bj-isrvec2  37985  bj-bary1  37997  icorempo  38038  isbasisrelowllem1  38042  isbasisrelowllem2  38043  relowlpssretop  38051  finxpsuclem  38084  pibt2  38104  poimirlem31  38343  isbnd2  38475  bfplem2  38515  ghomco  38583  cnf1dd  38780  contrd  38787  mpobi123f  38852  mptbi12f  38856  iss2  39034  refressn  39223  jca2r  39670  prter2  39696  lshpset2N  39934  cvrnbtwn2  40090  cvrnbtwn3  40091  cvrnbtwn4  40094  cvlcvr1  40154  hlrelat2  40218  cvrat4  40258  islpln2a  40363  linepsubN  40567  elpaddn0  40615  paddssw2  40659  pmapjoin  40667  ispsubcl2N  40762  dochkrshp  42201  dochsatshp  42266  mapdh9a  42604  hdmap11lem2  42657  sn-sup2  43306  frlmfzowrdb  43319  pwinfi3  44330  clsk1independent  44813  gneispace  44901  pm11.71  45148  relpmin  45702  ormkglobd  47632  2reu8i  47891  sbgoldbaltlem2  48586  oppcendc  49837  setrec1lem4  50509