Theorem 3adant3r3 1205

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  ressress  14781  plttr  15799  plelttr  15801  latledi  15918  latmlej11  15919  latmlej21  15921  latmlej22  15922  latjass  15924  latj12  15925  latj31  15928  ipopos  15989  latdisdlem  16018  imasmnd2  16156  imasmnd  16157  grpaddsubass  16327  grpsubsub4  16330  grpnpncan  16332  imasgrp2  16384  imasgrp  16385  frgp0  16977  cmn12  17017  abladdsub  17024  imasring  17463  dvrass  17534  lss1  17780  islmhm2  17879  psrgrp  18246  psrlmod  18249  zntoslem  18768  ipdir  18847  t1sep  20038  mettri2  21010  xmetrtri  21024  xmetrtri2  21025  pi1grplem  21715  dchrabl  23727  motgrp  24131  xmstrkgc  24391  ax5seglem4  24437  grpomuldivass  25449  grpopnpcan2  25453  grponpncan  25455  grpodiveq  25456  ablomuldiv  25489  ablodivdiv4  25491  nvadd12  25714  nvmdi  25743  nvsubadd  25748  nvmtri2  25773  dipdi  25956  dipsubdir  25961  dipsubdi  25962  cgr3tr4  29930  cgr3rflx  29932  seglemin  29991  linerflx1  30027  elicc3  30375  rngosubdi  30596  rngosubdir  30597  igenval2  30703  dmncan1  30713  mendlmod  31383  lincsumscmcl  33288  latmassOLD  35351  omlfh1N  35380  omlfh3N  35381  cvrnbtwn  35393  cvrnbtwn2  35397  cvrnbtwn4  35401  hlatj12  35492  cvrntr  35546  islpln2a  35669  3atnelvolN  35707  elpadd2at2  35928  paddasslem17  35957  paddass  35959  paddssw2  35965  pmapjlln1  35976  ltrn2ateq  36302  cdlemc3  36315  cdleme1b  36348  cdleme3b  36351  cdleme3c  36352  cdleme9b  36374  erngdvlem3  37113  erngdvlem3-rN  37121  dvalveclem  37149