Theorem 3adant3 811

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 797	. 2 |- ((ph /\ ps /\ th) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 10	1 |- ((ph /\ ps /\ th) -> ch)

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3adantl3 817  wereu 3002  ordunel 3141  funopg 3604  fnco 3652  f1ocnvfvb 3939  f1ofveu 3940  oprabvalig 4082  oprabval6g 4090  curry1val 4158  oaword 4241  omord2 4256  omcan 4258  omword 4259  omwordi 4260  oneo 4270  oeord 4273  oecan 4274  oeword 4275  oewordi 4276  ecopoprtrn 4372  eceqopreq 4374  abfii2 4622  zfregs 4709  ltsopi 5081  ltsopq 5140  genpass 5177  ltsopr 5201  ltsosr 5268  ltasr 5274  ltsor 5326  add12 5401  addcan2 5418  addsub 5449  npncan 5465  nppcan 5466  subcan 5477  mul12 5483  subdi 5492  nnncan1 5532  ppncan 5546  axlttrn 5569  axltadd 5570  ltso 5577  lelttr 5588  xrltso 5619  xrlelttr 5627  xrre2 5635  ltaddsub2 5697  leaddsub2 5699  lesub2 5726  ltsub2 5728  recextlem2 5748  divass 5804  div23 5805  divcan4 5820  divsubdir 5832  divsubdirOLD 5833  divcan5 5839  letrp1 5874  lemul1 5890  lemul1a 5895  lemul1aOLD 5896  ltmulgt12 5905  lediv1 5909  lediv1OLD 5910  ltmuldiv2OLD 5924  lt2mul2div 5931  lemuldivOLD 5935  lemuldiv2OLD 5937  ltdiv2 5947  lediv2 5951  xrmaxlt 5973  maxle 5978  maxlt 5982  nndivtr 6021  lbinfmle 6132  infmrcl 6151  xrsupsslem 6158  xrinfmsslem 6159  supxrre 6165  supxrun 6167  qsqueeze 6333  iooss2 6399  elioo5 6409  iccsupr 6424  lbicc2 6430  ubicc2 6431  iccneg 6433  icoshf 6434  ioojoin 6442  infmssuzle 6491  fzrevral2 6546  fzshftral 6548  seq1rn2 6580  shftval2 6606  shftf 6610  seqzp1 6637  seqzval2 6642  expsub 6687  expordi 6689  expwordi 6692  expword2i 6694  exple1 6696  expubnd 6697  bernneq2 6742  mulre 6867  abssubne0 6972  abssubge0 6985  abssuble0 6986  caurei 7017  cauimi 7018  ser1absdifi 7020  bcval2 7049  bccmpl 7052  fsum1ps 7108  fsum0spl 7111  fsumshf 7121  fsumshftm 7122  serz1p 7142  serzsplit 7146  climmullem3 7212  climmullem4 7213  climmullem5 7214  iserzgt0 7301  expcnv 7323  geoisum1c 7335  cvgratlem5 7344  rescncf 7362  cncffvrn 7363  mulc1cncf 7369  ivthlem6 7376  ivthlem7 7377  sin01gt0 7568  cos01gt0 7569  sin02gt0 7570  tgss2 7726  clsss 7772  clsss2 7788  elcls 7789  ntrcls0 7792  neiint 7804  neiss 7808  neips 7812  opnssneib 7814  innei 7821  islp2 7832  cnpval 7844  iscnp 7845  cncnp 7863  cncnp2 7864  metsym 7901  metxplem3 7913  metxplem4 7918  blin 7937  ssbl 7940  methausi 7966  metcnpf 7968  metcnf 7969  metcnp 7972  metcnss 7983  metdnsconst 7986  cnmet 7989  bl2ioo 7996  ioo2bl 7997  blssioo 7998  tgioolem 7999  dscmet 8003  lmbrf 8015  lmuni 8036  iscms2lem3 8076  iscms2lem4 8077  grpinvid1 8156  grpinvid2 8157  grpasscan1 8161  grpinvop 8164  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  grplactval 8181  ablnncan 8196  issubgi 8206  ablmul 8215  ghgrpilem4 8220  ringsn 8247  vcsubdir 8259  vcnegsubdi2 8278  vcoprnelem 8281  isvc 8284  isnv 8315  nvscom 8334  nvmul0or 8356  nvpncan2 8360  nvaddsub4 8365  nvnncan 8367  nvdif 8377  nvpi 8378  nvabs 8385  nv1 8388  imsmetlem 8407  nvelbl 8409  nvcnf 8411  nvcnpf 8412  va1cnlem 8429  nmoval 8510  0oval 8532  lnon0 8542  blometi 8547  ipasslem5 8578  hlipgt0 8700  ssphl 8703  pslem 8731  psasym 8735  pstr 8736  spwval3 8738  spwnex3 8739  spwpr4OLD 8746  spwpr4aOLD 8747  pilem1 8754  sinq12gt0t 8791  sincosq1eq 8792  efifolem5 8809  efif1lem1 8813  efif1lem2 8814  explog 8855  grothinf 8864  hvadd12 8987  hvmulcom 8995  hvsubdistr1 8999  hvsubdistr2 9000  hvaddcan2 9021  hvmulcan 9022  hvmulcan2 9023  hvsubcan 9024  hvsubcan2 9025  his7 9039  his2sub 9041  his2sub2 9042  bcs2 9132  bcs3 9133  hcau2 9138  hhssnv 9217  projlem26 9294  chj12 9540  spansncol 9574  pjspansn 9583  cm2j 9646  homul12 9814  hoaddsub 9825  unopf1o 9923  adj2 9941  braadd 9952  eigvalcl 9968  lnopmulsubi 9983  hmopco 10031  nmcopexlem5 10038  nmcfnexlem5 10067  cnlnadjlem2 10084  adjlnop 10102  kbass2 10133  leopmul 10150  leoptr 10153  hstoh 10243  strlem3a 10263  hstrlem3a 10271  cvntr 10303  dmdsl3 10326  atexch 10392  atcvatlem 10396  mdsymlem5 10418  cdj3lem2 10446  cdj3lem3 10449  lediv2aALT 10456  ghomgsg 10480  ghomf1olem 10481  symggrpi 10491  elo 10530  infi1 10532  cnrscoa 10604  ishomeo 10611  cmphmp 10615  cnvhmpha 10619  cnvhmphb 10620  hmphtr 10625  hmeogrp 10632  homcard 10633  hmeobc 10636  neifil 10661  filintf 10662  cnfilca 10670  sfvlim 10684  plimfilOLD 10688  usinuniop 10703  dmse1 10705  mslb1 10711  msra3 10713  eqidob 10805  cmphmib 10809  cmpassoh 10811  cmpmon 10825  iepiclem 10833  isfunb 10839

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232  df-3an 789

Copyright terms: Public domain