Theorem 3adant3r3 1193

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3adant3r3	|- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Proof of Theorem 3adant3r3

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1183	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1144	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960

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 185  df-an 371  df-3an 962

This theorem is referenced by:  ressress  14231  plttr  15136  plelttr  15138  latledi  15255  latmlej11  15256  latmlej21  15258  latmlej22  15259  latjass  15261  latj12  15262  latj31  15265  ipopos  15326  latdisdlem  15355  ismndd  15440  imasmnd2  15454  imasmnd  15455  grpaddsubass  15608  grpsubsub4  15611  grpnpncan  15613  imasgrp2  15663  imasgrp  15664  frgp0  16250  cmn12  16290  abladdsub  16297  imasrng  16701  dvrass  16772  lss1  16998  islmhm2  17097  psrgrp  17447  psrlmod  17450  zntoslem  17948  ipdir  18027  t1sep  18933  mettri2  19875  xmetrtri  19889  xmetrtri2  19890  pi1grplem  20580  dchrabl  22552  ax5seglem4  23113  grpomuldivass  23671  grpopnpcan2  23675  grponpncan  23677  grpodiveq  23678  ablomuldiv  23711  ablodivdiv4  23713  nvadd12  23936  nvmdi  23965  nvsubadd  23970  nvmtri2  23995  dipdi  24178  dipsubdir  24183  dipsubdi  24184  cgr3tr4  28012  cgr3rflx  28014  seglemin  28073  linerflx1  28109  elicc3  28437  rngosubdi  28684  rngosubdir  28685  igenval2  28791  dmncan1  28801  mendlmod  29475  lincsumscmcl  30808  latmassOLD  32596  omlfh1N  32625  omlfh3N  32626  cvrnbtwn  32638  cvrnbtwn2  32642  cvrnbtwn4  32646  hlatj12  32737  cvrntr  32791  islpln2a  32914  3atnelvolN  32952  elpadd2at2  33173  paddasslem17  33202  paddass  33204  paddssw2  33210  pmapjlln1  33221  ltrn2ateq  33546  cdlemc3  33559  cdleme1b  33592  cdleme3b  33595  cdleme3c  33596  cdleme9b  33618  erngdvlem3  34356  erngdvlem3-rN  34364  dvalveclem  34392