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  5083  iss  5994  oneqmini  6370  funssres  6536  elpreima  7004  isomin  7285  oneqmin  7747  frxp  8069  soseq  8102  tposfo2  8192  oa00  8487  odi  8507  oneo  8509  oeordsuc  8523  oelim2  8524  nnarcl  8545  nnmord  8561  nnneo  8584  map0g  8825  pssnn  9096  fodomfib  9232  fodomfibOLD  9234  inf3lem4  9543  cplem1  9804  karden  9810  alephordi  9987  cardinfima  10010  dfac5lem5  10040  isf34lem4  10290  axcc4  10352  axdc3lem2  10364  zorn2lem4  10412  zorn2lem7  10415  indpi  10821  genpcl  10922  addclprlem2  10931  ltaddpr  10948  ltexprlem5  10954  suplem1pr  10966  ltlen  11238  dedekind  11300  mulgt1OLD  12005  sup2  12103  nominpos  12405  uzind  12612  xrmaxlt  13124  xrltmin  13125  xrmaxle  13126  xrlemin  13127  xmullem2  13208  ccatopth  14669  shftuz  15022  sqreulem  15313  limsupbnd2  15436  mulcn2  15549  sadcaddlem  16417  dvdsgcdb  16505  algcvgblem  16537  lcmdvdsb  16573  rpexp  16683  infpnlem1  16872  divsfval  17502  iscatd  17630  posasymb  18276  plttr  18297  joinle  18341  meetle  18355  latnlej  18413  latnlej2  18416  lsmlub  19630  imasring  20301  unitmulclb  20352  lbspss  21069  lspsneu  21113  lspprat  21143  assapropd  21861  isclo2  23063  cncls2  23248  cncls  23249  cnntr  23250  cnrest2  23261  cmpsub  23375  cmpcld  23377  kgenss  23518  ptpjpre1  23546  txlm  23623  qtoptop2  23674  cmphaushmeo  23775  fbun  23815  isfild  23833  fbasrn  23859  fgtr  23865  ufinffr  23904  rnelfm  23928  fmfnfmlem4  23932  ghmcnp  24090  metrest  24499  icoopnst  24916  iocopnst  24917  dvfsumlem2  26004  dgreq0  26240  plyexmo  26290  taylthlem2  26351  cxpeq0  26655  mumullem2  27157  chpchtsum  27196  bposlem7  27267  lgsqr  27328  ltsres  27640  nosupno  27681  noinfno  27696  ltlesnd  27753  uspgr2wlkeq  29729  wwlknllvtx  29929  ex-natded5.3-2  30493  ubthlem1  30956  axhcompl-zf  31084  ococss  31379  nmopun  32100  elpjrn  32276  stm1addi  32331  stm1add3i  32333  mdsl1i  32407  chrelat2i  32451  atexch  32467  atcvat4i  32483  mdsymlem3  32491  bian1dOLD  32541  bnj600  35077  trssfir1om  35271  trssfir1omregs  35296  subgrwlk  35330  pthacycspth  35355  subfacval2  35385  climuzcnv  35869  3jcadALT  35885  fundmpss  35965  segconeq  36208  ifscgr  36242  endofsegid  36283  colinbtwnle  36316  trer  36514  ivthALT  36533  fnessref  36555  fnemeet2  36565  fnejoin2  36567  onsuct0  36639  bj-ideqg1  37494  bj-elid6  37500  bj-finsumval0  37615  bj-isrvec2  37630  bj-bary1  37642  icorempo  37681  isbasisrelowllem1  37685  isbasisrelowllem2  37686  relowlpssretop  37694  finxpsuclem  37727  pibt2  37747  poimirlem31  37986  isbnd2  38118  bfplem2  38158  ghomco  38226  cnf1dd  38425  contrd  38432  mpobi123f  38497  mptbi12f  38501  iss2  38679  refressn  38868  jca2r  39315  prter2  39341  lshpset2N  39579  cvrnbtwn2  39735  cvrnbtwn3  39736  cvrnbtwn4  39739  cvlcvr1  39799  hlrelat2  39863  cvrat4  39903  islpln2a  40008  linepsubN  40212  elpaddn0  40260  paddssw2  40304  pmapjoin  40312  ispsubcl2N  40407  dochkrshp  41846  dochsatshp  41911  mapdh9a  42249  hdmap11lem2  42302  sn-sup2  42950  frlmfzowrdb  42963  pwinfi3  44008  clsk1independent  44491  gneispace  44579  pm11.71  44842  relpmin  45397  ormkglobd  47321  2reu8i  47573  sbgoldbaltlem2  48268  oppcendc  49505  setrec1lem4  50177