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  2644  2eu1v  2645  disjxiun  5092  iss  5990  oneqmini  6364  funssres  6530  elpreima  6996  isomin  7278  oneqmin  7740  frxp  8066  soseq  8099  tposfo2  8189  oa00  8484  odi  8504  oneo  8506  oeordsuc  8519  oelim2  8520  nnarcl  8541  nnmord  8557  nnneo  8580  map0g  8818  pssnn  9092  fodomfib  9238  fodomfibOLD  9240  inf3lem4  9546  cplem1  9804  karden  9810  alephordi  9987  cardinfima  10010  dfac5lem5  10040  isf34lem4  10290  axcc4  10352  axdc3lem2  10364  zorn2lem4  10412  zorn2lem7  10415  indpi  10820  genpcl  10921  addclprlem2  10930  ltaddpr  10947  ltexprlem5  10953  suplem1pr  10965  ltlen  11235  dedekind  11297  mulgt1OLD  12001  sup2  12099  nominpos  12379  uzind  12586  xrmaxlt  13101  xrltmin  13102  xrmaxle  13103  xrlemin  13104  xmullem2  13185  ccatopth  14640  shftuz  14994  sqreulem  15285  limsupbnd2  15408  mulcn2  15521  sadcaddlem  16386  dvdsgcdb  16474  algcvgblem  16506  lcmdvdsb  16542  rpexp  16651  infpnlem1  16840  divsfval  17469  iscatd  17597  posasymb  18243  plttr  18264  joinle  18308  meetle  18322  latnlej  18380  latnlej2  18383  lsmlub  19561  imasring  20233  unitmulclb  20284  lbspss  21004  lspsneu  21048  lspprat  21078  assapropd  21797  isclo2  22991  cncls2  23176  cncls  23177  cnntr  23178  cnrest2  23189  cmpsub  23303  cmpcld  23305  kgenss  23446  ptpjpre1  23474  txlm  23551  qtoptop2  23602  cmphaushmeo  23703  fbun  23743  isfild  23761  fbasrn  23787  fgtr  23793  ufinffr  23832  rnelfm  23856  fmfnfmlem4  23860  ghmcnp  24018  metrest  24428  icoopnst  24852  iocopnst  24853  dvfsumlem2  25949  dgreq0  26187  plyexmo  26237  taylthlem2  26298  cxpeq0  26603  mumullem2  27106  chpchtsum  27146  bposlem7  27217  lgsqr  27278  sltres  27590  nosupno  27631  noinfno  27646  sltlend  27699  uspgr2wlkeq  29609  wwlknllvtx  29809  ex-natded5.3-2  30370  ubthlem1  30832  axhcompl-zf  30960  ococss  31255  nmopun  31976  elpjrn  32152  stm1addi  32207  stm1add3i  32209  mdsl1i  32283  chrelat2i  32327  atexch  32343  atcvat4i  32359  mdsymlem3  32367  bian1dOLD  32419  bnj600  34885  subgrwlk  35104  pthacycspth  35129  subfacval2  35159  climuzcnv  35643  3jcadALT  35659  fundmpss  35739  segconeq  35983  ifscgr  36017  endofsegid  36058  colinbtwnle  36091  trer  36289  ivthALT  36308  fnessref  36330  fnemeet2  36340  fnejoin2  36342  onsuct0  36414  bj-ideqg1  37137  bj-elid6  37143  bj-finsumval0  37258  bj-isrvec2  37273  bj-bary1  37285  icorempo  37324  isbasisrelowllem1  37328  isbasisrelowllem2  37329  relowlpssretop  37337  finxpsuclem  37370  pibt2  37390  poimirlem31  37630  isbnd2  37762  bfplem2  37802  ghomco  37870  cnf1dd  38069  contrd  38076  mpobi123f  38141  mptbi12f  38145  iss2  38311  refressn  38419  jca2r  38833  prter2  38859  lshpset2N  39097  cvrnbtwn2  39253  cvrnbtwn3  39254  cvrnbtwn4  39257  cvlcvr1  39317  hlrelat2  39382  cvrat4  39422  islpln2a  39527  linepsubN  39731  elpaddn0  39779  paddssw2  39823  pmapjoin  39831  ispsubcl2N  39926  dochkrshp  41365  dochsatshp  41430  mapdh9a  41768  hdmap11lem2  41821  sn-sup2  42464  frlmfzowrdb  42477  pwinfi3  43536  clsk1independent  44019  gneispace  44107  pm11.71  44370  relpmin  44926  ormkglobd  46857  tworepnotupword  46868  2reu8i  47098  sbgoldbaltlem2  47765  oppcendc  49004  setrec1lem4  49676