Theorem 3adant3 798

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 784	. 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 223   /\ w3a 774

This theorem is referenced by:  3adantl3 804  wereu 2941  ordunel 3080  funopg 3543  fnco 3591  f1ocnvfvb 3876  f1ofveu 3877  oprabvalig 4019  oprabval6g 4027  curry1val 4093  oaword 4176  omord2 4191  omcan 4193  omword 4194  omwordi 4195  oneo 4205  oeord 4208  oecan 4209  oeword 4210  oewordi 4211  ecopoprtrn 4304  eceqopreq 4306  abfii2 4545  zfregs 4630  ltsopi 4999  ltsopq 5058  genpass 5095  ltsopr 5119  ltsosr 5186  ltasr 5192  ltsor 5244  add12t 5319  addcan2t 5336  addsubt 5367  npncant 5383  nppcant 5384  subcant 5395  mul12t 5401  subdit 5410  nnncan1t 5450  ppncant 5464  axlttrn 5487  axltadd 5488  ltso 5495  lelttrt 5506  xrltso 5537  xrlelttrt 5545  xrre2t 5553  ltaddsub2t 5616  leaddsub2t 5618  lesub2t 5644  ltsub2t 5646  recextlem2 5666  div23t 5715  divcan4t 5729  divsubdirt 5741  divcan5t 5747  letrp1t 5782  lemul1t 5798  lemul1it 5803  lemul1itOLD 5804  ltmulgt12t 5813  lediv1t 5816  ltmuldiv2t 5828  lt2mul2divt 5832  lemuldivt 5834  lemuldiv2t 5835  ltdiv2t 5845  lediv2t 5849  xrmaxltt 5871  maxlet 5876  maxltt 5880  nndivtrt 5917  lbinfmle 6007  infmrcl 6026  xrsupsslem 6033  xrinfmsslem 6034  supxrre 6040  supxrun 6042  qsqueeze 6230  seq1rn2 6271  shftval2t 6297  shftf 6301  iooss2 6324  iccsupr 6344  lbicc2t 6350  ubicc2t 6351  ioonegt 6352  iccnegt 6353  icoshft 6354  infmssuzle 6410  fzrevral2t 6465  fzshftralt 6467  seqzp1 6493  seqzval2t 6498  expsubt 6543  expordit 6545  expwordit 6548  expword2it 6550  exple1t 6552  expubndt 6553  bernneq2 6598  abssubne0t 6835  abssubge0t 6848  abssuble0t 6849  caure 6879  cauim 6880  ser1absdif 6882  bcval2t 6912  bccmplt 6915  fsum1ps 6971  fsum0split 6974  fsumshft 6984  fsumshftm 6985  serz1p 7005  serzsplit 7009  climmullem3 7075  climmullem4 7076  climmullem5 7077  iserzgt0 7163  expcnv 7185  geoisum1c 7197  cvgratlem5 7206  rescncf 7224  cncffvrn 7225  mulc1cncf 7231  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  sin01gt0 7435  cos01gt0 7436  sin02gt0 7437  tgss2t 7597  clsss 7647  clsss2 7663  elcls 7664  ntrcls0 7667  neiint 7679  neiss 7683  neips 7687  opnssneib 7689  innei 7696  islp2 7707  cnpval 7719  iscnp 7720  cncnp 7738  cncnp2 7739  metsym 7776  metxplem3 7790  metxplem4 7795  blin 7814  ssbl 7817  methausi 7843  metcnpf 7845  metcnf 7846  metcnp 7849  metcnss 7860  metdnsconst 7863  cnmet 7866  bl2ioo 7873  ioo2bl 7874  blssioo 7875  tgioolem 7876  dscmet 7880  lmbrf 7892  lmuni 7913  iscms2lem3 7953  iscms2lem4 7954  grpinvid1 8034  grpinvid2 8035  grpasscan1 8039  grpinvop 8042  grppncan 8052  grpnpcan 8053  grppnpcan2 8054  grplactval 8060  ablnncan 8076  issubgi 8086  ablmul 8095  ghgrpilem4 8100  ringsn 8127  vcsubdir 8139  vcnegsubdi2 8158  vcoprnelem 8161  isvc 8164  isnv 8195  nvscom 8214  nvmul0or 8236  nvpncan2 8240  nvaddsub4 8245  nvnncan 8247  nvdif 8257  nvpi 8258  nvabs 8265  nv1 8268  imsmetlem 8287  nvelbl 8289  nvcnf 8291  nvcnpf 8292  va1cnlem 8307  nmoval 8386  0oval 8408  blometi 8422  ipasslem5 8453  hlipgt0 8574  ssphl 8577  pslem 8605  psasym 8608  pstr 8609  spwval3 8611  spwnex3 8612  pilem1 8625  sinq12gt0t 8660  sincosq1eq 8661  efifolem5 8676  efif1lem1 8680  efif1lem2 8681  circgrpOLD 8693  explogt 8727  grothinf 8736  hvadd12t 8859  hvmulcomt 8867  hvsubdistr1t 8871  hvsubdistr2t 8872  hvaddcan2t 8893  hvmulcant 8894  hvmulcan2t 8895  hvsubcant 8896  hvsubcan2t 8897  his7t 8911  his2subt 8913  his2sub2t 8914  bcs2t 9004  bcs3t 9005  hcau2 9010  hhssnv 9089  projlem26 9166  chj12t 9412  spansncol 9447  pjspansnt 9457  cm2jt 9520  homul12t 9688  hoaddsubt 9699  unopf1ot 9797  adj2t 9815  braaddt 9826  eigvalclt 9842  lnopmulsub 9857  hmopcot 9904  nmcopexlem5 9911  nmcfnexlem5 9940  cnlnadjlem2 9957  adjlnopt 9975  kbass2t 10006  leopmult 10023  leoptrt 10026  hstoht 10115  strlem3a 10135  hstrlem3a 10143  cvntrt 10175  dmdsl3t 10198  atexcht 10264  atcvatlem 10268  mdsymlem5 10290  cdj3lem2 10318  cdj3lem3 10321  lediv2itALT 10327  ghomgsg 10351  ghomf1olem 10352  symggrpi 10362  elo 10403  infi1 10405  cnrscoa 10456  ishomeo 10463  cmphmp 10467  cnvhmpha 10471  cnvhmphb 10472  hmphtr 10477  hmeogrp 10484  homcard 10485  neifil 10501  filintf 10502  cnfilca 10510  plimfil 10525  dmse1 10539  mslb1 10545  msra3 10547  eqidob 10639  cmphmib 10643  cmpassoh 10645  cmpmon 10657  isfunb 10665

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 147  df-an 225  df-3an 776

Copyright terms: Public domain