Theorem 3adant3r3 1207

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

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

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 975

This theorem is referenced by:  ressress  14548  plttr  15453  plelttr  15455  latledi  15572  latmlej11  15573  latmlej21  15575  latmlej22  15576  latjass  15578  latj12  15579  latj31  15582  ipopos  15643  latdisdlem  15672  ismndd  15757  imasmnd2  15771  imasmnd  15772  grpaddsubass  15929  grpsubsub4  15932  grpnpncan  15934  imasgrp2  15985  imasgrp  15986  frgp0  16574  cmn12  16614  abladdsub  16621  imasrng  17052  dvrass  17123  lss1  17368  islmhm2  17467  psrgrp  17822  psrlmod  17825  zntoslem  18362  ipdir  18441  t1sep  19637  mettri2  20579  xmetrtri  20593  xmetrtri2  20594  pi1grplem  21284  dchrabl  23257  motgrp  23658  ax5seglem4  23911  grpomuldivass  24927  grpopnpcan2  24931  grponpncan  24933  grpodiveq  24934  ablomuldiv  24967  ablodivdiv4  24969  nvadd12  25192  nvmdi  25221  nvsubadd  25226  nvmtri2  25251  dipdi  25434  dipsubdir  25439  dipsubdi  25440  cgr3tr4  29279  cgr3rflx  29281  seglemin  29340  linerflx1  29376  elicc3  29712  rngosubdi  29959  rngosubdir  29960  igenval2  30066  dmncan1  30076  mendlmod  30747  lincsumscmcl  32107  latmassOLD  34026  omlfh1N  34055  omlfh3N  34056  cvrnbtwn  34068  cvrnbtwn2  34072  cvrnbtwn4  34076  hlatj12  34167  cvrntr  34221  islpln2a  34344  3atnelvolN  34382  elpadd2at2  34603  paddasslem17  34632  paddass  34634  paddssw2  34640  pmapjlln1  34651  ltrn2ateq  34976  cdlemc3  34989  cdleme1b  35022  cdleme3b  35025  cdleme3c  35026  cdleme9b  35048  erngdvlem3  35786  erngdvlem3-rN  35794  dvalveclem  35822