Theorem 3ad2antl1 1223

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantlr 751	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl2 1218	1 |- ( ( ( ph /\ ps /\ ta ) /\ 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:  smorndom  7465  omeulem1  7662  dif1en  8193  ordiso2  8420  infpssrlem4  9128  fin1a2lem9  9230  gchpwdom  9492  tskwun  9606  gruxp  9629  infregelb  11007  fzo1fzo0n0  12518  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fprodle  14727  muldvds2  15007  dvds2add  15015  dvds2sub  15016  dvdstr  15018  lcmfledvds  15345  mulgnnsubcl  17553  mulgpropd  17584  gexdvdsi  17998  ringidss  18577  reslmhm2  19053  issubassa  19324  obs2ss  20073  lsslindf  20169  mndvcl  20197  mhmvlin  20203  madurid  20450  restntr  20986  cnpnei  21068  upxp  21426  qtopss  21518  opnfbas  21646  fbasrn  21688  trfg  21695  ufilmax  21711  ustuqtop1  22045  prdsxmetlem  22173  nmoix  22533  nmoi2  22534  iimulcl  22736  mbfimaopn2  23424  lgsval4lem  25033  f1otrg  25751  brbtwn2  25785  colinearalg  25790  axsegconlem1  25797  0vtxrusgr  26473  clwwlksfo  26918  clwwisshclwws  26928  numclwlk1lem2foa  27224  numclwlk1lem2fo  27228  lnosub  27614  pjspansn  28436  eulerpartlemb  30430  cnpconn  31212  mclspps  31481  nodenselem8  31841  curf  33387  mblfinlem2  33447  mblfinlem3  33448  mettrifi  33553  ghomdiv  33691  grpokerinj  33692  rngohomco  33773  crngohomfo  33805  keridl  33831  cvrcon3b  34564  mzpsubst  37311  lzunuz  37331  diophrex  37339  rmxycomplete  37482  jm2.26  37569  lnmepi  37655  lmhmlnmsplit  37657  ntrclsiso  38365  ntrclskb  38367  ntrclsk3  38368  uzwo4  39221  wessf1ornlem  39371  choicefi  39392  supxrgere  39549  supxrgelem  39553  supxrge  39554  suplesup  39555  infxr  39583  infleinflem2  39587  rexabslelem  39645  fmul01lt1  39818  limcleqr  39876  limclner  39883  dvnprodlem1  40161  volioc  40188  stoweidlem60  40277  wallispilem3  40284  fourierdlem12  40336  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem54  40377  fourierdlem68  40391  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem83  40406  elaa2  40451  etransclem24  40475  etransclem32  40483  ioorrnopnlem  40524  issalnnd  40563  sge0xaddlem2  40651  sge0seq  40663  meaiininc2  40702  hoicvr  40762  ovnsubaddlem2  40785  hoidmvval0  40801  hoidmvlelem3  40811  hspmbllem2  40841  vonioo  40896  vonicc  40899  smfinflem  41023  fmtnoprmfac2lem1  41478  fmtnofac1  41482  lincresunit3lem3  42263  suppdm  42300