Theorem 3adant3r3 1226

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 1216	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3adantr3 1175	1 |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  ressress  15242  plttr  16271  plelttr  16273  latledi  16390  latmlej11  16391  latmlej21  16393  latmlej22  16394  latjass  16396  latj12  16397  latj31  16400  ipopos  16461  latdisdlem  16490  imasmnd2  16628  imasmnd  16629  grpaddsubass  16799  grpsubsub4  16802  grpnpncan  16804  imasgrp2  16856  imasgrp  16857  frgp0  17465  cmn12  17505  abladdsub  17512  imasring  17902  dvrass  17973  lss1  18217  islmhm2  18316  psrgrp  18677  psrlmod  18680  zntoslem  19182  ipdir  19261  t1sep  20441  mettri2  21411  xmetrtri  21425  xmetrtri2  21426  pi1grplem  22135  dchrabl  24238  motgrp  24644  xmstrkgc  24972  ax5seglem4  25018  grpomuldivass  26033  grpopnpcan2  26037  grponpncan  26039  grpodiveq  26040  ablomuldiv  26073  ablodivdiv4  26075  nvadd12  26298  nvmdi  26327  nvsubadd  26332  nvmtri2  26357  dipdi  26540  dipsubdir  26545  dipsubdi  26546  cgr3tr4  30869  cgr3rflx  30871  seglemin  30930  linerflx1  30966  elicc3  31023  rngosubdi  32238  rngosubdir  32239  igenval2  32345  dmncan1  32355  latmassOLD  32841  omlfh1N  32870  omlfh3N  32871  cvrnbtwn  32883  cvrnbtwn2  32887  cvrnbtwn4  32891  hlatj12  32982  cvrntr  33036  islpln2a  33159  3atnelvolN  33197  elpadd2at2  33418  paddasslem17  33447  paddass  33449  paddssw2  33455  pmapjlln1  33466  ltrn2ateq  33792  cdlemc3  33805  cdleme1b  33838  cdleme3b  33841  cdleme3c  33842  cdleme9b  33864  erngdvlem3  34603  erngdvlem3-rN  34611  dvalveclem  34639  mendlmod  36105  lincsumscmcl  40595