Theorem 3adant2 1167

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 1146	. 2 |- ((ph /\ th /\ ps) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 13	1 |- ((ph /\ th /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130

This theorem is referenced by:  3ad2ant1 1169  3adantl2OLD 1307  eupickb 2126  ordunel 4080  funopg 4594  fnco 4658  dff1o2 4766  fnimapr 4852  f1ocnvfvb 4991  oprssoprv 5097  curry1val 5239  poxp 5252  smoiso 5313  oaord 5432  oaword 5434  omcan 5451  omwordri 5454  odi 5461  omeulem1 5464  oecan 5470  oewordri 5473  oeordsuc 5475  nnaordr 5494  ecopoprtrn 5574  eceqopreq 5576  fodomr 5759  findcard 5887  fimax 5890  r111 6050  carden2b 6187  dif1cardOLD 6209  cfeq0 6342  cfsuc 6343  cfflb 6346  cflim2 6350  cfsmolem 6352  axcc3 6362  axcc3OLD 6364  domtriomlem 6365  domtriomlemOLD 6366  domtriomlemOLDOLD 6369  axdc3lem2 6377  axdc3lem4 6379  axdc4lem 6381  axcclem 6383  pwcfsdom 6527  ltsopi 6611  ltsopq 6670  ltsopr 6731  ltsosr 6798  ltasr 6804  adddir 6925  axlttrn 6965  letr 6986  xrletr 7025  subcan2 7157  subcan 7167  subdi 7174  subdir 7175  nnncan1 7206  pnpcan2 7218  pnncan 7219  ltadd2 7248  leadd2 7250  lesub1 7284  lesub2 7285  ltsub1 7286  ltsub2 7287  mulcan2 7315  div23 7358  div13 7359  divsubdir 7384  ltmul2 7442  ltmul2OLD 7443  lemul1 7444  lemul1OLD 7445  lemul2 7446  lemul2OLD 7447  lemul2a 7454  lemul2aOLD 7455  lediv1 7468  ltmuldiv2 7482  lt2mul2divOLD 7490  lemuldiv 7493  lemuldiv2 7494  ltdiv2 7505  lediv2 7509  nndivtr 7579  bndndx 7734  supxrbnd 7752  fnn0ind 7881  uzwo3lem1 7886  qsqueeze 7919  modmulnn 7968  modcyc 7974  moddi 7978  modsubdir 7979  iooss1 7998  iooss2 7999  eliooord 8014  iooneg 8033  iccneg 8034  icoshft 8035  ioojoin 8043  lbzbi 8110  fzen 8139  elfz2nn0 8144  fzrev2i 8168  fzrevral2 8184  fzshftral 8186  shftval2 8251  expsub 8341  expsubOLD 8342  expdiv 8344  expwordi 8348  expword2i 8350  expubnd 8353  bernneq2 8400  abs3dif 8652  seq1ubi 8665  fsumshft 8803  fsumshftm 8804  caucvglem2 8930  isummulc1iALT 8986  supcvglem 8992  supcvglemOLD 8994  cvgratlem5 9032  cncffvrn 9051  sin02gt0 9260  infxpidmlem4OLD 9354  infxp 9371  dvdscmul 9406  dvdsmulc 9407  dvdscmulr 9408  dvdsmulcr 9409  divalglem8 9433  ndvdssub 9440  mulgcdlem2 9488  isprm3 9506  coprmdvds 9514  prmdvdsexpb 9520  1arithlem19 9548  1arithprmb 9552  grpinvid1 9646  grpinvid2 9647  ple1 9757  latleeqj1 9775  clatl 9826  lubun 9832  clatleglb 9835  istps3OLD 9864  istps3 9869  subbas2 9916  iincld 9968  neiint 10010  elnei 10016  islp2 10039  cnco 10061  cncnp 10071  cnconst 10073  metsym 10109  metge0 10112  metxplem3 10121  metxplem4 10126  blin 10145  ssbl 10148  metcnpf 10177  metcnp 10181  metcnpi3 10186  metcnpi4 10187  metcnss 10192  metcnss2 10193  cnmet 10198  dscmet 10212  lmuni 10245  metcnp4 10265  metcnp4OLD 10266  iscms2lem4 10288  isgrpo 10339  grpoinvid1 10377  grpoinvid2 10378  grpasscan1 10382  grpinvop 10386  grpdivinv 10389  grpinvdiv 10390  grpdivf 10391  grppncan 10396  grpnpcan 10397  grppnpcan2 10398  gxnn0suc 10408  gxid 10417  resgrprn 10424  ablnncan 10441  vcnegsubdi2 10547  vcsub4 10548  nvmval 10616  nvmul0or 10625  nvsubadd 10628  nvpncan2 10629  nvaddsub4 10634  nvnncan 10636  nvmeq0 10637  nvdif 10646  nvpi 10647  nvmtri 10652  nvabs 10654  imsmetlem 10676  nvelbl 10678  nvcnpf 10681  nvlmle 10686  va1cnlem 10705  ipval2lem3 10715  ipval2 10717  4ipval2 10718  ipval3 10719  ipval2lem6 10721  nvcnpi3 10782  nvcnpi4 10783  nmoge0 10790  blometi 10826  htthlem8 11001  pslem 11017  psasym 11021  pstr 11022  spwcl 11030  spwpr4c 11036  efifolem6 11108  efif1lem1 11111  efif1lem2 11112  fiiu2 11213  uptx 11219  txcn 11220  txcnopab 11221  fgfil 11286  limfilss 11295  neifil 11298  hvaddsub12 11535  hvsubdistr1 11544  hvsubdistr2 11545  hvaddcan2 11566  hvmulcan 11567  hvmulcan2 11568  hvsubcan 11569  hvsubcan2 11570  his7 11584  his2sub 11586  his2sub2 11587  norm3dif2 11645  hcau2 11682  shsubcl 11715  hhssnv 11759  shlej2 11981  pjspansn 12125  hodcl 12148  fh2 12185  cm2j 12186  pjoi0 12287  hosubdi 12361  unopf1o 12467  unopadj 12470  adj2 12485  braadd 12496  bramul 12497  lnopaddmuli 12524  lnopsubmuli 12526  lnfnaddmuli 12601  adjlnop 12646  leopmul 12694  leoptr 12697  pjimai 12737  atcv1 12941  atexch 12942  atcvatlem 12946  bnj625 13570  bnj839 13642  adderpqlem 14557  mulerpqlem 14558  mulcanenq 14563  distrnq 14564  ltsonq 14572  ltanq 14574  ltmnq 14575  prmdvdsexpbOLD 14602  ghomf1olem 14621  sindivcvglem2 14634  sindivcvglem3 14635  modaddabs 14657  lediv2aALT 14660  fununiq 14723  tz6.26 14805  poxpOLD 14849  wfrlem4 14860  sltres 14917  elfuns 15021  fiiu 15313  njtlc 15360  surrc2 15361  surjsec 15435  mapmapmap 15486  injsurinj 15487  preodom2 15567  preoran2 15571  altprs2 15577  nfwpr4c 15630  fprod1ib 15686  fprodadd 15709  ablinvop 15710  grpdlcan 15735  grpdivzer 15736  cmprtr 15755  prsubrtr 15758  cmpltr 15767  cmperltr 15772  rltrran 15777  multinv 15785  zerdivemp1 15799  mulinvsca 15837  svli2 15840  nelioo5 15870  cnrsfin 15886  cnrscoa 15887  cmphmp 15896  hmphtr 15903  homcard 15911  intcont 15940  fgsb 15948  fgsb2 15952  conttnf 15971  iscnp3 15973  exopcopn 15982  topgrpbs 16013  tpgprop2 16026  lrtrhom 16028  grphm 16035  lvsovso 16093  supnuf 16096  dualcat2 16188  eqidob 16199  cmphmia 16202  ismonc 16218  isepic 16228  cptarc 16313  tarsuc2 16316  tartarmap 16336  fnctartar 16355  fnctartar2 16356  eqeu 16436  ioodisj 16449  ntrin 16496  clsun 16498  neiin 16503  cncls 16504  subsubtop 16508  compsublem 16515  fnetr 16580  reftr 16582  refssfne 16589  topmtcl 16610  supfil 16645  ufilen 16664  ufcondr 16666  flimcls 16673  fmfnfmlem1 16679  fmfnfmlem2 16680  fmfnfmlem4 16682  fmfnfm 16683  fclusss 16696  fnimaprOLD 16772  f1elima 16804  upixp 16814  eroprv 16819  fimaxOLD 16831  filbcmb 16861  fzsplit 16877  iihalf1 16957  iihalf2 16958  icoopnst 16961  iocopnst 16962  cncfco 16972  hmeocn 16982  lmtlm 16993  heiborlem18 17057  bfp 17094  grpeqdivid 17123  ghomco 17125  pcohtpy 17168  pcopt 17169  ringnegrmul 17190  zerdivemp1x 17193  rnghomco 17213  rngisoco 17221  riscer 17227  intidl 17262  isfldidl 17301  smoisoOLD 17536  lubunNEW 17826  opnlen0 17845  glb0 17849  opcon3b 17852  opcon2b 17853  oplecon3b 17856  opltcon3b 17860  opltcon2b 17862  oldmm1 17873  oldmm4 17876  oldmj1 17877  oldmj4 17880  cvrval2 17927  cvrcon3b 17930  leat 17945  atcmpOLD 17953  atcvreq0OLD 17956  atcmp 17970  atcvreq0 17973  atlatle 17980  athgt 18117  3dim2 18129  islln2a 18217  lplnnleat 18246  lvolnleat 18287  4atlem10 18310  4atlem11 18313  4atlem12 18316  dalem21 18398  dalem22 18399  dalem23 18400  dalem29 18405  dalem30 18406  dalem31 18407  dalem32 18408  dalem33 18409  dalem34 18410  dalem35 18411  dalem36 18412  dalem37 18413  dalem40 18416  dalem46 18422  dalem47 18423  dalem51 18427  dalem52 18428  dalem58 18434  dalem59 18435  pmaple 18465  paddcl 18546  pmapjoin 18556  pmapjat1 18557  2polcon4b 18607  paddun 18613  poldmj1 18614  pmapj2 18615  pmapocj 18616  psubclin 18634  paddatcl 18635  poml4 18638  lautco 18731  ltrn2ateq 18848  cdlemgfvawOLD 19260

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 232  df-an 435  df-3an 1132

Copyright terms: Public domain