Theorem 3adantl3 1146

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 985	. 2 |- ( ( ph /\ ps /\ ta ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 471	1 |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )

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

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 967

This theorem is referenced by:  dif1enOLD  7544  dif1en  7545  infpssrlem4  8475  fin23lem11  8486  tskwun  8951  gruf  8978  lediv2a  10226  prunioo  11414  rpnnen2lem7  13503  muldvds1  13557  muldvds2  13558  dvdscmul  13559  dvdsmulc  13560  rpexp  13806  pospropd  15304  mdetmul  18429  elcls  18677  iscnp4  18867  cnpnei  18868  cnpflf2  19573  cnpflf  19574  cnpfcf  19614  xbln0  19989  blcls  20081  iimulcl  20509  icccvx  20522  iscau2  20788  rrxcph  20896  cncombf  21136  mumul  22519  f1otrg  23117  ax5seglem1  23174  ax5seglem2  23175  nvmul0or  24032  fh1  25021  fh2  25022  cm2j  25023  pjoi0  25120  hoadddi  25207  hmopco  25427  iocinif  26071  volfiniune  26646  eulerpartlemb  26751  cnambfre  28440  ivthALT  28530  rngohomco  28780  rngoisoco  28788  ibliccsinexp  29791  iblioosinexp  29793  wwlkext2clwwlk  30465  lincdifsn  30958  pexmidlem3N  33616  hdmapglem7  35577