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  1056  2eu1  2649  2eu1v  2650  disjxiun  5145  iss  6055  oneqmini  6438  funssres  6612  elpreima  7078  isomin  7357  oneqmin  7820  frxp  8150  soseq  8183  tposfo2  8273  oa00  8596  odi  8616  oneo  8618  oeordsuc  8631  oelim2  8632  nnarcl  8653  nnmord  8669  nnneo  8692  map0g  8923  pssnn  9207  onomeneqOLD  9264  fodomfib  9367  fodomfibOLD  9369  inf3lem4  9669  cplem1  9927  karden  9933  alephordi  10112  cardinfima  10135  dfac5lem5  10165  isf34lem4  10415  axcc4  10477  axdc3lem2  10489  zorn2lem4  10537  zorn2lem7  10540  indpi  10945  genpcl  11046  addclprlem2  11055  ltaddpr  11072  ltexprlem5  11078  suplem1pr  11090  ltlen  11360  dedekind  11422  mulgt1OLD  12124  sup2  12222  nominpos  12501  uzind  12708  xrmaxlt  13220  xrltmin  13221  xrmaxle  13222  xrlemin  13223  xmullem2  13304  ccatopth  14751  shftuz  15105  sqreulem  15395  limsupbnd2  15516  mulcn2  15629  sadcaddlem  16491  dvdsgcdb  16579  algcvgblem  16611  lcmdvdsb  16647  rpexp  16756  infpnlem1  16944  divsfval  17594  iscatd  17718  posasymb  18377  plttr  18400  joinle  18444  meetle  18458  latnlej  18514  latnlej2  18517  lsmlub  19697  imasring  20344  unitmulclb  20398  lbspss  21099  lspsneu  21143  lspprat  21173  assapropd  21910  isclo2  23112  cncls2  23297  cncls  23298  cnntr  23299  cnrest2  23310  cmpsub  23424  cmpcld  23426  kgenss  23567  ptpjpre1  23595  txlm  23672  qtoptop2  23723  cmphaushmeo  23824  fbun  23864  isfild  23882  fbasrn  23908  fgtr  23914  ufinffr  23953  rnelfm  23977  fmfnfmlem4  23981  ghmcnp  24139  metrest  24553  icoopnst  24983  iocopnst  24984  dvfsumlem2  26082  dgreq0  26320  plyexmo  26370  taylthlem2  26431  cxpeq0  26735  mumullem2  27238  chpchtsum  27278  bposlem7  27349  lgsqr  27410  sltres  27722  nosupno  27763  noinfno  27778  sltlend  27831  uspgr2wlkeq  29679  wwlknllvtx  29876  ex-natded5.3-2  30437  ubthlem1  30899  axhcompl-zf  31027  ococss  31322  nmopun  32043  elpjrn  32219  stm1addi  32274  stm1add3i  32276  mdsl1i  32350  chrelat2i  32394  atexch  32410  atcvat4i  32426  mdsymlem3  32434  bian1dOLD  32485  bnj600  34912  subgrwlk  35117  pthacycspth  35142  subfacval2  35172  climuzcnv  35656  3jcadALT  35672  fundmpss  35748  segconeq  35992  ifscgr  36026  endofsegid  36067  colinbtwnle  36100  trer  36299  ivthALT  36318  fnessref  36340  fnemeet2  36350  fnejoin2  36352  onsuct0  36424  bj-ideqg1  37147  bj-elid6  37153  bj-finsumval0  37268  bj-isrvec2  37283  bj-bary1  37295  icorempo  37334  isbasisrelowllem1  37338  isbasisrelowllem2  37339  relowlpssretop  37347  finxpsuclem  37380  pibt2  37400  poimirlem31  37638  isbnd2  37770  bfplem2  37810  ghomco  37878  cnf1dd  38077  contrd  38084  mpobi123f  38149  mptbi12f  38153  iss2  38326  refressn  38425  jca2r  38837  prter2  38863  lshpset2N  39101  cvrnbtwn2  39257  cvrnbtwn3  39258  cvrnbtwn4  39261  cvlcvr1  39321  hlrelat2  39386  cvrat4  39426  islpln2a  39531  linepsubN  39735  elpaddn0  39783  paddssw2  39827  pmapjoin  39835  ispsubcl2N  39930  dochkrshp  41369  dochsatshp  41434  mapdh9a  41772  hdmap11lem2  41825  sn-sup2  42478  frlmfzowrdb  42491  pwinfi3  43553  clsk1independent  44036  gneispace  44124  pm11.71  44393  tworepnotupword  46840  2reu8i  47063  sbgoldbaltlem2  47705  setrec1lem4  48921