Theorem 3adantl3 1165

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3simpa 1004	. 2 |- ( ( ph /\ ps /\ ta ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 474	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 984

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 189  df-an 373  df-3an 986

This theorem is referenced by:  dif1en  7801  infpssrlem4  8733  fin23lem11  8744  tskwun  9206  gruf  9233  lediv2a  10497  prunioo  11758  rpnnen2lem7  14266  muldvds1  14320  muldvds2  14321  dvdscmul  14322  dvdsmulc  14323  rpexp  14665  pospropd  16373  mdetmul  19641  elcls  20082  iscnp4  20272  cnpnei  20273  cnpflf2  21008  cnpflf  21009  cnpfcf  21049  xbln0  21422  blcls  21514  iimulcl  21958  icccvx  21971  iscau2  22240  rrxcph  22344  cncombf  22607  mumul  24101  ax5seglem1  24951  ax5seglem2  24952  wwlkext2clwwlk  25524  nvmul0or  26266  fh1  27264  fh2  27265  cm2j  27266  pjoi0  27363  hoadddi  27449  hmopco  27669  padct  28300  iocinif  28356  volfiniune  29046  eulerpartlemb  29194  ivthALT  30984  cnambfre  31982  rngohomco  32206  rngoisoco  32214  pexmidlem3N  33531  hdmapglem7  35494  relexpmulg  36296  supxrgere  37550  supxrgelem  37554  supxrge  37555  lptre2pt  37714  dvnprodlem1  37815  ibliccsinexp  37821  iblioosinexp  37823  fourierdlem12  37975  fourierdlem41  38005  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem48  38012  fourierdlem49  38013  fourierdlem51  38015  fourierdlem73  38037  fourierdlem74  38038  fourierdlem75  38039  fourierdlem97  38061  etransclem24  38117  sge0rpcpnf  38257  lincdifsn  40204