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  2651  2eu1v  2652  disjxiun  5082  iss  6000  oneqmini  6376  funssres  6542  elpreima  7010  isomin  7292  oneqmin  7754  frxp  8076  soseq  8109  tposfo2  8199  oa00  8494  odi  8514  oneo  8516  oeordsuc  8530  oelim2  8531  nnarcl  8552  nnmord  8568  nnneo  8591  map0g  8832  pssnn  9103  fodomfib  9239  fodomfibOLD  9241  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  11247  dedekind  11309  mulgt1OLD  12014  sup2  12112  nominpos  12414  uzind  12621  xrmaxlt  13133  xrltmin  13134  xrmaxle  13135  xrlemin  13136  xmullem2  13217  ccatopth  14678  shftuz  15031  sqreulem  15322  limsupbnd2  15445  mulcn2  15558  sadcaddlem  16426  dvdsgcdb  16514  algcvgblem  16546  lcmdvdsb  16582  rpexp  16692  infpnlem1  16881  divsfval  17511  iscatd  17639  posasymb  18285  plttr  18306  joinle  18350  meetle  18364  latnlej  18422  latnlej2  18425  lsmlub  19639  imasring  20310  unitmulclb  20361  lbspss  21077  lspsneu  21121  lspprat  21151  assapropd  21851  isclo2  23053  cncls2  23238  cncls  23239  cnntr  23240  cnrest2  23251  cmpsub  23365  cmpcld  23367  kgenss  23508  ptpjpre1  23536  txlm  23613  qtoptop2  23664  cmphaushmeo  23765  fbun  23805  isfild  23823  fbasrn  23849  fgtr  23855  ufinffr  23894  rnelfm  23918  fmfnfmlem4  23922  ghmcnp  24080  metrest  24489  icoopnst  24906  iocopnst  24907  dvfsumlem2  25994  dgreq0  26230  plyexmo  26279  taylthlem2  26339  cxpeq0  26642  mumullem2  27143  chpchtsum  27182  bposlem7  27253  lgsqr  27314  ltsres  27626  nosupno  27667  noinfno  27682  ltlesnd  27739  uspgr2wlkeq  29714  wwlknllvtx  29914  ex-natded5.3-2  30478  ubthlem1  30941  axhcompl-zf  31069  ococss  31364  nmopun  32085  elpjrn  32261  stm1addi  32316  stm1add3i  32318  mdsl1i  32392  chrelat2i  32436  atexch  32452  atcvat4i  32468  mdsymlem3  32476  bian1dOLD  32526  bnj600  35061  trssfir1om  35255  trssfir1omregs  35280  subgrwlk  35314  pthacycspth  35339  subfacval2  35369  climuzcnv  35853  3jcadALT  35869  fundmpss  35949  segconeq  36192  ifscgr  36226  endofsegid  36267  colinbtwnle  36300  trer  36498  ivthALT  36517  fnessref  36539  fnemeet2  36549  fnejoin2  36551  onsuct0  36623  bj-ideqg1  37478  bj-elid6  37484  bj-finsumval0  37599  bj-isrvec2  37614  bj-bary1  37626  icorempo  37667  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlpssretop  37680  finxpsuclem  37713  pibt2  37733  poimirlem31  37972  isbnd2  38104  bfplem2  38144  ghomco  38212  cnf1dd  38411  contrd  38418  mpobi123f  38483  mptbi12f  38487  iss2  38665  refressn  38854  jca2r  39301  prter2  39327  lshpset2N  39565  cvrnbtwn2  39721  cvrnbtwn3  39722  cvrnbtwn4  39725  cvlcvr1  39785  hlrelat2  39849  cvrat4  39889  islpln2a  39994  linepsubN  40198  elpaddn0  40246  paddssw2  40290  pmapjoin  40298  ispsubcl2N  40393  dochkrshp  41832  dochsatshp  41897  mapdh9a  42235  hdmap11lem2  42288  sn-sup2  42936  frlmfzowrdb  42949  pwinfi3  43990  clsk1independent  44473  gneispace  44561  pm11.71  44824  relpmin  45379  ormkglobd  47305  2reu8i  47561  sbgoldbaltlem2  48256  oppcendc  49493  setrec1lem4  50165