Theorem 3adant1r 1319

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant1r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3expb 1266	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	adantlr 751	. 2 |- ( ( ( ph /\ ta ) /\ ( ps /\ ch ) ) -> th )
4	3	3impb 1260	1 |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3adant2r  1321  3adant3r  1323  ecopovtrn  7850  isf32lem9  9183  axdc3lem4  9275  tskun  9608  dvdscmulr  15010  divalglem8  15123  ghmgrp  17539  quscrng  19240  dvfsumlem3  23791  dvfsumrlim  23794  dvfsumrlim2  23795  dvfsumrlim3  23796  dchrisumlem3  25180  dchrisum  25181  abvcxp  25304  padicabv  25319  hvmulcan  27929  isarchi2  29739  archiabllem2c  29749  hasheuni  30147  carsgclctunlem1  30379  carsggect  30380  carsgclctunlem2  30381  carsgclctunlem3  30382  carsgclctun  30383  carsgsiga  30384  omsmeas  30385  tendoicl  36084  cdlemkfid2N  36211  erngdvlem4  36279  pellex  37399  refsumcn  39189  restuni3  39301  wessf1ornlem  39371  unirnmapsn  39406  ssmapsn  39408  iunmapsn  39409  ssfiunibd  39523  supxrgelem  39553  infleinf2  39641  fmuldfeq  39815  limsupmnfuzlem  39958  limsupre3uzlem  39967  cosknegpi  40080  icccncfext  40100  stoweidlem31  40248  stoweidlem43  40260  stoweidlem46  40263  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  stoweidlem55  40272  stoweidlem56  40273  stoweidlem57  40274  stoweidlem58  40275  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  stoweid  40280  fourierdlem12  40336  fourierdlem41  40365  fourierdlem48  40371  fourierdlem79  40402  fourierdlem81  40404  etransclem24  40475  etransclem46  40497  sge0f1o  40599  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0seq  40663  caragenfiiuncl  40729  hoicvr  40762  hoidmvval0  40801  hspmbllem2  40841  smflimsuplem7  41032  el0ldep  42255