Theorem 3adant3r3 1216

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  ressress  15172  plttr  16201  plelttr  16203  latledi  16320  latmlej11  16321  latmlej21  16323  latmlej22  16324  latjass  16326  latj12  16327  latj31  16330  ipopos  16391  latdisdlem  16420  imasmnd2  16558  imasmnd  16559  grpaddsubass  16729  grpsubsub4  16732  grpnpncan  16734  imasgrp2  16786  imasgrp  16787  frgp0  17395  cmn12  17435  abladdsub  17442  imasring  17832  dvrass  17903  lss1  18147  islmhm2  18246  psrgrp  18607  psrlmod  18610  zntoslem  19111  ipdir  19190  t1sep  20370  mettri2  21340  xmetrtri  21354  xmetrtri2  21355  pi1grplem  22064  dchrabl  24166  motgrp  24572  xmstrkgc  24900  ax5seglem4  24946  grpomuldivass  25960  grpopnpcan2  25964  grponpncan  25966  grpodiveq  25967  ablomuldiv  26000  ablodivdiv4  26002  nvadd12  26225  nvmdi  26254  nvsubadd  26259  nvmtri2  26284  dipdi  26467  dipsubdir  26472  dipsubdi  26473  cgr3tr4  30809  cgr3rflx  30811  seglemin  30870  linerflx1  30906  elicc3  30963  rngosubdi  32103  rngosubdir  32104  igenval2  32210  dmncan1  32220  latmassOLD  32711  omlfh1N  32740  omlfh3N  32741  cvrnbtwn  32753  cvrnbtwn2  32757  cvrnbtwn4  32761  hlatj12  32852  cvrntr  32906  islpln2a  33029  3atnelvolN  33067  elpadd2at2  33288  paddasslem17  33317  paddass  33319  paddssw2  33325  pmapjlln1  33336  ltrn2ateq  33662  cdlemc3  33675  cdleme1b  33708  cdleme3b  33711  cdleme3c  33712  cdleme9b  33734  erngdvlem3  34473  erngdvlem3-rN  34481  dvalveclem  34509  mendlmod  35976  lincsumscmcl  39414