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  2676  2eu1v  2677  disjxiun  5100  iss  6029  oneqmini  6409  funssres  6576  elpreima  7049  isomin  7337  oneqmin  7803  frxp  8127  soseq  8160  tposfo2  8250  oa00  8551  odi  8571  oneo  8573  oeordsuc  8587  oelim2  8588  nnarcl  8609  nnmord  8625  nnneo  8648  map0g  8896  pssnn  9168  fodomfib  9304  inf3lem4  9616  cplem1  9931  cplem1OLD  9932  kardenOLD  9941  setrec1lem4  9952  alephordi  10134  cardinfima  10157  dfac5lem5  10187  isf34lem4  10436  axcc4  10498  axdc3lem2  10510  zorn2lem4  10558  zorn2lem7  10561  indpi  10973  genpcl  11074  addclprlem2  11083  ltaddpr  11100  ltexprlem5  11106  suplem1pr  11118  ltlen  11392  dedekind  11454  sup2  12254  nominpos  12564  uzind  12772  xrmaxlt  13292  xrltmin  13293  xrmaxle  13294  xrlemin  13295  xmullem2  13376  ccatopth  14845  shftuz  15202  sqreulem  15507  limsupbnd2  15630  mulcn2  15743  sadcaddlem  16607  dvdsgcdb  16698  algcvgblem  16732  lcmdvdsb  16768  rpexp  16878  infpnlem1  17068  divsfval  17699  iscatd  17827  posasymb  18473  plttr  18494  joinle  18538  meetle  18552  latnlej  18610  latnlej2  18613  lsmlub  19858  imasring  20540  unitmulclb  20591  lbspss  21337  lspsneu  21381  lspprat  21411  assapropd  22159  isclo2  23386  cncls2  23571  cncls  23572  cnntr  23573  cnrest2  23584  cmpsub  23698  cmpcld  23700  kgenss  23842  ptpjpre1  23870  txlm  23947  qtoptop2  23998  cmphaushmeo  24099  fbun  24139  isfild  24157  fbasrn  24183  fgtr  24189  ufinffr  24228  rnelfm  24252  fmfnfmlem4  24256  ghmcnp  24414  metrest  24823  icoopnst  25240  iocopnst  25241  dvfsumlem2  26327  dgreq0  26564  plyexmo  26618  taylthlem2  26683  cxpeq0  26988  mumullem2  27489  chpchtsum  27528  bposlem7  27599  lgsqr  27660  ltsres  28001  nosupno  28042  noinfno  28057  ltlesnd  28114  uspgr2wlkeq  30208  subgrwlk  30251  wwlknllvtx  30417  ex-natded5.3-2  30991  ubthlem1  31454  axhcompl-zf  31582  ococss  31877  nmopun  32598  elpjrn  32774  stm1addi  32829  stm1add3i  32831  mdsl1i  32905  chrelat2i  32949  atexch  32965  atcvat4i  32981  mdsymlem3  32989  bnj600  35532  trssfir1om  35716  trssfir1omregs  35777  karddom  35802  kardsdom  35803  pthacycspth  35891  subfacval2  35921  climuzcnv  36405  3jcadALT  36421  fundmpss  36501  segconeq  36745  ifscgr  36779  endofsegid  36820  colinbtwnle  36853  trer  37074  ivthALT  37093  fnessref  37115  fnemeet2  37125  fnejoin2  37127  onsuct0  37199  bj-ideqg1  38053  bj-elid6  38059  bj-finsumval0  38174  bj-isrvec2  38189  bj-bary1  38201  icorempo  38242  isbasisrelowllem1  38246  isbasisrelowllem2  38247  relowlpssretop  38255  finxpsuclem  38288  pibt2  38308  poimirlem31  38537  isbnd2  38685  bfplem2  38725  ghomco  38793  cnf1dd  38990  contrd  38997  mpobi123f  39062  mptbi12f  39066  iss2  39244  refressn  39433  jca2r  39880  prter2  39906  lshpset2N  40144  cvrnbtwn2  40300  cvrnbtwn3  40301  cvrnbtwn4  40304  cvlcvr1  40364  hlrelat2  40428  cvrat4  40468  islpln2a  40573  linepsubN  40777  elpaddn0  40825  paddssw2  40869  pmapjoin  40877  ispsubcl2N  40972  dochkrshp  42411  dochsatshp  42476  mapdh9a  42814  hdmap11lem2  42867  sn-sup2  43523  frlmfzowrdb  43536  pwinfi3  44522  clsk1independent  45005  gneispace  45093  pm11.71  45340  relpmin  45894  ormkglobd  47831  2reu8i  48127  sbgoldbaltlem2  48822  oppcendc  50070