Theorem 3adant3 896

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 872	. 2 |- ((ph /\ ps /\ th) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 12	1 |- ((ph /\ ps /\ th) -> ch)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3adantl3 1034  wereu 3654  ordunel 3906  funopg 4454  fnco 4521  resdif 4659  f1ocnvfvb 4857  f1ofveu 4858  oprabvalig 4953  oprabval6g 4962  curry1val 5077  curry2val 5080  onfununi 5116  oaword 5230  oawordOLD 5231  omord2 5246  omcan 5248  omword 5249  omwordi 5250  oneo 5260  oeord 5263  oecan 5264  oeword 5265  oewordi 5266  ecopoprtrn 5370  eceqopreq 5372  abfii2 5652  hartog 5693  zfregs 5754  omsubindss 5888  nnacda 6088  nnaun 6089  ltsopi 6168  ltsopq 6227  genpass 6264  ltsopr 6288  ltsosr 6355  ltasr 6361  ltsor 6413  add12 6489  addcan2 6508  addsub 6542  addsubOLD 6543  npncan 6560  nppcan 6561  subcan 6572  mul12 6579  subdi 6590  nnncan1OLD 6633  ppncan 6648  axlttrn 6673  axltadd 6674  ltso 6681  lelttr 6693  xrltso 6729  xrlelttr 6737  xrre2 6745  ltaddsub2 6815  leaddsub2 6817  lesub2 6850  ltsub2 6852  recextlem2 6875  divass 6924  div23 6925  divcan4 6939  divsubdir 6951  divcan5 6957  divdiv23 6969  divdiv2 6973  letrp1 6994  lemul1 7011  lemul1OLD 7012  lemul1a 7019  lemul1aOLD 7020  ltmulgt12 7029  lediv1 7033  lediv1OLD 7034  ltmuldiv2OLD 7048  lt2mul2divOLD 7055  lemuldiv2OLD 7060  ltdiv2 7070  lediv2 7074  ltdiv23 7075  lediv23 7076  xrmaxlt 7096  maxle 7101  maxlt 7105  lbinfmle 7259  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  supxrun 7294  qsqueeze 7461  modmulnn 7510  modabs 7514  moddi 7520  modsubdir 7521  iooss2 7541  elioo5 7552  iccsupr 7567  lbicc2 7573  ubicc2 7574  iccneg 7576  icoshft 7577  ioojoin 7585  infmssuzleOLD 7635  fzen 7664  fzsuc 7678  fzrevral2 7699  fzshftral 7701  seq1rn2 7734  shftval2 7760  shftf 7764  seqzp1 7791  seqzval2 7796  expsub 7841  expsubOLD 7842  expdiv 7844  expordi 7845  expwordi 7848  expword2i 7850  exple1 7852  expubnd 7853  bernneq2 7900  mulre 8027  abssubne0 8134  abssubge0 8147  abssuble0 8148  caurei 8179  cauimi 8180  ser1absdifi 8182  bcval2 8211  bccmpl 8214  fsum1ps 8278  fsum0split 8281  fsumshft 8291  fsumshftm 8292  serz1p 8312  serzsplit 8316  climmullem3 8382  climmullem4 8383  climmullem5 8384  iserzgt0 8472  expcnv 8494  explecnv 8495  cvgratlem5 8516  rescncf 8534  cncffvrn 8535  mulc1cncf 8541  ivthlem6 8548  ivthlem7 8549  sin01gt0 8742  cos01gt0 8743  sin02gt0 8744  tgss2 8907  clsss 8963  clsss2 8979  elcls 8980  ntrcls0 8983  neiint 8995  neiss 8999  neips 9003  opnssneib 9005  innei 9012  islp2 9023  cnpval 9035  iscnp 9036  cncnp 9055  cncnp2 9056  metsym 9093  metxplem3 9105  metxplem4 9110  blin 9129  ssbl 9132  methausi 9159  metcnpf 9161  metcnf 9162  metcnp 9165  metcnss 9176  metdnsconst 9179  cnmet 9182  bl2ioo 9189  ioo2bl 9190  blssioo 9191  tgioolem 9192  dscmet 9196  lmbrf 9208  lmuni 9229  iscms2lem3 9269  iscms2lem4 9270  grpinvid1 9356  grpinvid2 9357  grpasscan1 9361  grpinvop 9365  grppncan 9375  grpnpcan 9376  grppnpcan2 9377  gxnn0suc 9387  gxcl 9388  gxinv 9393  gxinv2 9394  gxsuc 9395  gxid 9396  gxnn0add 9397  gxnn0mul 9400  grplactval 9405  ablnncan 9420  issubgi 9431  ablmul 9439  ghgrpilem4 9444  isga 9450  isga2 9452  gapmlem 9461  gapm 9462  ringsn 9490  vcsubdir 9507  vcnegsubdi2 9526  vcoprnelem 9529  isvc 9532  isnv 9563  nvscom 9582  nvmul0or 9604  nvpncan2 9608  nvaddsub4 9613  nvnncan 9615  nvdif 9625  nvpi 9626  nvabs 9633  nv1 9636  imsmetlem 9655  nvelbl 9657  nvcnf 9659  nvcnpf 9660  vacnlem3 9669  va1cnlem 9684  nmoval 9765  0oval 9788  lnon0 9798  blometi 9803  ipasslem5 9835  ajval 9863  hlipgt0 9963  ssphl 9966  pslem 9990  psasym 9994  pstr 9995  spwval3 9997  spwnex3 9998  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  pilem1 10020  sinq12gt0t 10057  sincosq1eq 10059  efifolem5 10080  efif1lem1 10084  efif1lem2 10085  explog 10126  grothpw 10134  grothpwex 10135  grothomex 10136  dif1en 10172  indexfi 10174  symggrpi 10205  uptx 10226  txcn 10227  ishomeo 10235  hmeobc 10239  cnvhmpha 10240  subtopmetlem 10255  subtopmet 10256  filintf 10274  fsubbas 10281  fgfil 10290  sfvlim 10296  limfil 10297  limfilss 10299  neifil 10302  hausfillim 10303  isfilmap 10308  filmapss 10309  sflimf 10318  flimfneii 10320  cncomp 10331  usinuniop 10341  hvadd12 10536  hvmulcom 10544  hvsubdistr1 10548  hvsubdistr2 10549  hvaddcan2 10570  hvmulcan 10571  hvmulcanOLD 10572  hvmulcan2 10573  hvsubcan 10574  hvsubcan2 10575  his7 10589  his2sub 10591  his2sub2 10592  bcs2 10682  bcs3 10683  hcau2 10688  hhssnv 10767  projlem26 10844  chj12 11090  spansncol 11124  pjspansn 11133  cm2j 11196  homul12 11368  hoaddsub 11379  unopf1o 11477  adj2 11495  braadd 11506  eigvalcl 11522  lnopmulsubi 11537  hmopco 11585  nmcopexlem5 11592  nmcfnexlem5 11621  cnlnadjlem2 11638  adjlnop 11656  kbass2 11688  leopmul 11705  leoptr 11708  hstoh 11804  strlem3a 11824  hstrlem3a 11832  cvntr 11864  dmdsl3 11887  atexch 11953  atcvatlem 11957  mdsymlem5 11979  cdj3lem2 12007  cdj3lem3 12010  bnj623 12640  bnj838 12712  bnj553 13278  bnj966 13348  bnj967 13349  bnj1125 13430  bnj1173 13441  lediv2aALT 13621  ghomgsg 13636  ghomf1olem 13637  dvdscmul 13680  dvdscmulr 13682  dvdsle 13693  dvdsleabs 13694  divalglem8 13703  divalgb 13707  mulgcdlem2 13757  prmdvdsmul 13784  poxp 13949  wfrlem3 13959  wfrlem4 13960  wfrlem9 13965  axdenselem8 14026  nocvxmin 14029  axfelem8 14038  axfelem9 14039  axfelem12 14042  oprssoprvg 14335  elo 14342  infi1 14343  njtlc 14389  surrc2 14390  inttrp 14437  valpr 14499  npincppr 14501  prjmapcp 14507  unprj 14511  prl 14512  prjmapcp2 14515  valcurfn1 14552  ubpar 14603  supdef 14604  supaub 14615  suplub2 14616  dffprod 14670  fprod1ib 14686  reacomsmgrp2 14704  clfsebs 14707  ablinvop 14714  gaplc 14731  gapm2 14732  fnopabco2b 14734  curgrpact 14735  grpdivone 14736  fprodneg 14741  prsubrtr 14763  multinvb 14772  zerdivemp1 14785  rngridfz 14786  svli2 14826  svs2 14829  islp3 14861  cnrscoa 14869  cmphmp 14878  cnvhmphb 14880  hmphtr 14885  hmeogrp 14892  homcard 14893  intcont 14914  cnfilca 14927  plimfil 14940  flimfneih 14942  bwt2 14960  tpgprop2 14987  dmse1 15001  mslb1 15007  msra3 15009  nolimf2 15032  lvsovso 15038  supnuf 15041  dualcat2lem 15129  dualded2lem 15130  dualcat2 15133  eqidob 15144  cmphmib 15148  cmpassoh 15150  cmpmon 15164  iepiclem 15172  isfunb 15183  elincin 15220  inacint 15221  tarax3c 15224  tarorpa 15236  vtare 15262  vtarsu 15263  vtarl 15264  tartarmap 15265  eqeu 15351  hartogOLD 15384  omsubindssOLD 15397  ntrin 15411  clsun 15413  neiin 15418  cncls 15419  cnntr 15420  subcls 15424  subntr 15425  compsublem 15430  cptclsscpt 15432  compfipin0lem 15435  compfipin0 15436  alexsub 15441  connsub 15443  reconnlem5 15450  reconn 15451  ivthALT 15454  2ndcctbss 15478  fness 15491  locfindsc 15515  opnfbas 15557  neifg 15559  ufprim 15569  ufinffr 15578  ufilen 15579  flimcls 15588  fmfnfmlem4 15597  fmfnfm 15598  fclusss 15611  sfclusf 15624  eltail 15635  fnimapr 15687  oprabvalg 15706  f1ocan1fv 15717  eroprv 15734  indexfiOLD 15755  fzmul 15790  fzsplit 15792  subspabs 15840  lpss2 15842  mettrifi2 15848  geomcau 15849  caushft 15851  iccsplit 15854  iihalf1 15872  iihalf2 15873  lincmb01cmp 15878  oprpiece1res2 15881  cncfco 15887  cnres2 15890  piececn 15894  hmeocnv 15898  tlmbrf 15905  txmet 15925  heiborlem10 15964  heiborlem18 15972  heiborlem22 15976  bfp 16009  exidreslem 16030  ghomco 16040  phtpycolem2 16052  phtpyco 16056  pcoval 16073  pcoval2 16075  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcorev 16087  pi1gp 16095  ringneglmul 16104  zerdivemp1x 16108  isdivrng2 16111  rnggrphom 16125  smprngpr 16200  smores2 16447  smoiso 16453  posasymb 16776  isposiNEW 16778  pleval2 16785  pltval3 16787  lubprop 16805  lubid 16807  glbprop 16810  p0le 16845  latleeqm1 16874  lubss 16897  lubun 16899  lubunNEW 16900  opcon3b 16923  oplecon3b 16927  oplecon1b 16928  opltcon3b 16931  opltcon1b 16932  olj01 16944  oldmm1 16946  oldmm2 16947  oldmj1 16950  oldmj2 16951  omllaw2 16965  omllaw3 16966  cmtcomlem 16969  omlfh1 16978  omlfh3 16979  cvrnbtwn2 16992  cvrnbtwn3 16993  cvrcon3b 16994  cvrnbtwn4 16996  leatom 17005  atomcmp 17008  atnlt 17009  atomcvreq0 17010  atncvr 17011  hlexchb 17035  hlatle 17048  hlrelat5 17050  atcvr0eq 17064  atexchlt 17074  isgrpiNEW 17115  grpinvid1NEW 17131  grpinvid2NEW 17132  pmaple 17241  pmapglbx 17251  elpaddri 17263  paddcl 17303  pmapjoin 17313  pmapjat 17314  polcon3 17330  2polcon4b 17331  polcon2 17332  paddun 17337  poldmj1 17338  pmapj2 17339  pmapocj 17340  psubclin 17357  paddatcl 17358  poml5 17362  osumcllem3 17366  osumcllem4 17367  osumcllem11 17374  pl42lem4 17410

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 164  df-an 242  df-3an 860

Copyright terms: Public domain