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  1057  2eu1  2652  2eu1v  2653  disjxiun  5097  iss  6002  oneqmini  6378  funssres  6544  elpreima  7012  isomin  7293  oneqmin  7755  frxp  8078  soseq  8111  tposfo2  8201  oa00  8496  odi  8516  oneo  8518  oeordsuc  8532  oelim2  8533  nnarcl  8554  nnmord  8570  nnneo  8593  map0g  8834  pssnn  9105  fodomfib  9241  fodomfibOLD  9243  inf3lem4  9552  cplem1  9813  karden  9819  alephordi  9996  cardinfima  10019  dfac5lem5  10049  isf34lem4  10299  axcc4  10361  axdc3lem2  10373  zorn2lem4  10421  zorn2lem7  10424  indpi  10830  genpcl  10931  addclprlem2  10940  ltaddpr  10957  ltexprlem5  10963  suplem1pr  10975  ltlen  11246  dedekind  11308  mulgt1OLD  12012  sup2  12110  nominpos  12390  uzind  12596  xrmaxlt  13108  xrltmin  13109  xrmaxle  13110  xrlemin  13111  xmullem2  13192  ccatopth  14651  shftuz  15004  sqreulem  15295  limsupbnd2  15418  mulcn2  15531  sadcaddlem  16396  dvdsgcdb  16484  algcvgblem  16516  lcmdvdsb  16552  rpexp  16661  infpnlem1  16850  divsfval  17480  iscatd  17608  posasymb  18254  plttr  18275  joinle  18319  meetle  18333  latnlej  18391  latnlej2  18394  lsmlub  19605  imasring  20278  unitmulclb  20329  lbspss  21046  lspsneu  21090  lspprat  21120  assapropd  21839  isclo2  23044  cncls2  23229  cncls  23230  cnntr  23231  cnrest2  23242  cmpsub  23356  cmpcld  23358  kgenss  23499  ptpjpre1  23527  txlm  23604  qtoptop2  23655  cmphaushmeo  23756  fbun  23796  isfild  23814  fbasrn  23840  fgtr  23846  ufinffr  23885  rnelfm  23909  fmfnfmlem4  23913  ghmcnp  24071  metrest  24480  icoopnst  24904  iocopnst  24905  dvfsumlem2  26001  dgreq0  26239  plyexmo  26289  taylthlem2  26350  cxpeq0  26655  mumullem2  27158  chpchtsum  27198  bposlem7  27269  lgsqr  27330  ltsres  27642  nosupno  27683  noinfno  27698  ltlesnd  27755  uspgr2wlkeq  29731  wwlknllvtx  29931  ex-natded5.3-2  30495  ubthlem1  30957  axhcompl-zf  31085  ococss  31380  nmopun  32101  elpjrn  32277  stm1addi  32332  stm1add3i  32334  mdsl1i  32408  chrelat2i  32452  atexch  32468  atcvat4i  32484  mdsymlem3  32492  bian1dOLD  32542  bnj600  35094  trssfir1om  35286  trssfir1omregs  35311  subgrwlk  35345  pthacycspth  35370  subfacval2  35400  climuzcnv  35884  3jcadALT  35900  fundmpss  35980  segconeq  36223  ifscgr  36257  endofsegid  36298  colinbtwnle  36331  trer  36529  ivthALT  36548  fnessref  36570  fnemeet2  36580  fnejoin2  36582  onsuct0  36654  bj-ideqg1  37413  bj-elid6  37419  bj-finsumval0  37534  bj-isrvec2  37549  bj-bary1  37561  icorempo  37600  isbasisrelowllem1  37604  isbasisrelowllem2  37605  relowlpssretop  37613  finxpsuclem  37646  pibt2  37666  poimirlem31  37896  isbnd2  38028  bfplem2  38068  ghomco  38136  cnf1dd  38335  contrd  38342  mpobi123f  38407  mptbi12f  38411  iss2  38589  refressn  38778  jca2r  39225  prter2  39251  lshpset2N  39489  cvrnbtwn2  39645  cvrnbtwn3  39646  cvrnbtwn4  39649  cvlcvr1  39709  hlrelat2  39773  cvrat4  39813  islpln2a  39918  linepsubN  40122  elpaddn0  40170  paddssw2  40214  pmapjoin  40222  ispsubcl2N  40317  dochkrshp  41756  dochsatshp  41821  mapdh9a  42159  hdmap11lem2  42212  sn-sup2  42855  frlmfzowrdb  42868  pwinfi3  43913  clsk1independent  44396  gneispace  44484  pm11.71  44747  relpmin  45302  ormkglobd  47227  2reu8i  47467  sbgoldbaltlem2  48134  oppcendc  49371  setrec1lem4  50043