Theorem 3ad2ant3 899

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	|- (ph -> ch)

Assertion

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

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantl 424	. 2 |- ((th /\ ph) -> ch)
3	2	3adant1 894	1 |- ((ps /\ th /\ ph) -> ch)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  simp3l 904  simp3r 905  simp31 912  simp32 913  simp33 914  simp3ll 947  simp3lr 948  simp3rl 949  simp3rr 950  simp3l1 981  simp3l2 982  simp3l3 983  simp3r1 984  simp3r2 985  simp3r3 986  simp31l 999  simp31r 1000  simp32l 1001  simp32r 1002  simp33l 1003  simp33r 1004  simp311 1023  simp312 1024  simp313 1025  simp321 1026  simp322 1027  simp323 1028  simp331 1029  simp332 1030  simp333 1031  3anibar 1044  3jaao 1164  limsuc 3933  oprabvalig 4953  curry1val 5077  curry2val 5080  omwordi 5250  oneo 5260  oewordi 5266  ac6sfilem3 5508  ordiso 5683  hartog 5693  en3lplem1 5756  nnacda 6088  cnegexlem2 6500  divcan5 6957  lemul1a 7019  lemul1aOLD 7020  lt2halves 7228  infmrcl 7278  zdivmul 7399  modabs 7514  modcyc 7516  moddi 7520  modsubdir 7521  elioo5 7552  iccsupr 7567  iccneg 7576  icoshft 7577  icoshftf1olem 7579  elfzlem 7643  fzen 7664  fzshftral 7701  expm1 7843  serzmulc1 8317  climge0 8372  explecnv 8495  cvgratlem2ALT 8510  cvgratlem2 8513  rescncf 8534  mulc1cncf 8541  demoivre 8752  tgss 8906  clsss 8963  ntrcls0 8983  neiss 8999  neips 9003  cnpval 9035  cnpnei 9043  elbl2 9116  lmbrf 9208  iscms2lem3 9269  gxpval 9382  gxnval 9383  gxnn0neg 9386  gxnn0suc 9387  gxneg 9389  gxsuc 9395  gxnn0add 9397  gxadd 9398  gxsub 9399  gxnn0mul 9400  gxmul 9401  gxmodid 9402  grplactval 9405  gxdi 9422  gafo 9451  gacan 9460  gapmlem 9461  gapm 9462  vcid 9502  vcdi 9503  vcdir 9504  vcass 9505  imsmetlem 9655  vacnlem3 9669  nmoval 9765  nmoubi 9774  0oval 9788  ajval 9863  spwval3 9997  spwnex3 9998  sincosq1eq 10059  oprabvaligg 10154  cardennn 10171  dif1en 10172  indexfi 10174  fiuni 10219  upxp 10225  uptx 10226  ishomeo 10235  subtopmetlem 10255  subtopmet 10256  filintf 10274  fgss 10287  extbas1 10291  limfil 10297  hausfillim 10303  filmapss 10309  fmf 10310  fmbas 10311  elfilmap 10312  elfilmap3 10314  flimfneii 10320  fbaslim 10322  cncomp 10331  usinuniop 10341  nmopub 11469  nmfnleub 11486  hmopco 11585  adjlnop 11656  mdslmd4i 11905  bnj837 12711  bnj1195 12976  bnj553 13278  bnj583 13296  bnj594 13300  bnj966 13348  bnj967 13349  bnj1097 13412  bnj1100 13414  bnj1108 13416  bnj1110 13417  bnj1118 13420  bnj1128 13428  bnj1125 13430  bnj1145 13431  bnj1137 13433  bnj1136 13435  bnj1173 13441  bnj1321 13498  bnj1410 13520  ghomf1olem 13637  suprzcl 13658  dfon2lem3 13851  dfon2lem7 13855  predso 13895  nnssi3 14257  nndivsub 14258  oprssoprvg 14335  elo 14342  infi1 14343  sndw 14428  inttrp 14437  surjsec2 14467  mapmapmap 14486  injsurinj 14487  valpr 14499  cbicplem 14508  unprj 14511  labs1 14536  labs2 14538  int2pre 14578  ubpar 14603  supdef 14604  supaub 14615  inposet 14620  nfwpr4c 14630  tostos 14637  toplat 14638  fprod1ib 14686  clfsebs 14707  fincmpzer 14711  fprodadd 14713  gaplc 14731  fnopabco2b 14734  curgrpact 14735  fprodneg 14741  fprodsub 14742  prsubrtr 14763  zerdivemp1 14785  rngridfz 14786  svli2 14826  hmphsyma 14882  fgsb 14921  cnfilca 14927  rcfpfil 14934  limfilnei 14943  conttnf 14944  conttnf2 14945  cnpfillim4 14947  altretop 14997  nolimf2 15032  lvsovso 15038  lvsovso3 15040  supnufb 15042  cmppfd 15092  1cat 15106  dualcat2 15133  imonclem 15162  ismonc 15163  iepiclem 15172  isepic 15173  isfunb 15183  idsubfun 15206  elincin 15220  cptarc 15242  sexptrt 15243  tarsuc1 15244  tarsuc2 15245  vtarsu 15263  vtarl 15264  tartarmap 15265  elfiun 15369  inficlALT 15372  ordisoOLD 15374  hartogOLD 15384  cncls 15419  cnntr 15420  cptclsscpt 15432  hscptsscld 15434  alexsub 15441  connsub 15443  ivthALT 15454  2ndcctbss 15478  ssref 15492  fnetr 15495  reftr 15497  refssfne 15504  locfindsc 15515  comppfsc 15517  neibastop1 15518  topmtcl 15525  fnemeet1 15528  ist1-2 15542  isnrm2 15552  opnfbas 15557  fgmin 15558  supfil 15560  filufint 15574  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  flimcls 15588  cnpfillim 15589  imaelfm 15591  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  filclus 15605  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  ufcomp 15622  eltail 15635  fimax 15746  indexfiOLD 15755  fisup2g 15768  filbcmb 15776  fsumlt1 15831  subspabs 15840  geomcau 15849  caushft 15851  iccsplit 15854  paste 15893  totbndss 15937  heiborlem10 15964  phtpyco 16056  pcohtpylem3 16082  pcorev 16087  pi1gp 16095  smprngpr 16200  igenval2 16214  smoel 16451  clatleglb 16903  cvrnbtwn 16990  atomcmp 17008  atomcvreq0 17010  atmnem0 17032  cvr1 17054  cvr2 17055  cvratlem 17061  pointpsub 17231  pmapglbx 17251  pmapjat 17314  paddatcl 17358  osumcllem4 17367  osumcllem7 17370

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