Theorem adantl 305

Description: Inference adding a conjunct to the left of an antecedent.

Hypothesis

Ref	Expression
adantl.1	|- (ph -> ps)

Assertion

Ref	Expression
adantl	|- ((ch /\ ph) -> ps)

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 |- (ph -> ps)
2	1	a1i 7	. 2 |- (ch -> (ph -> ps))
3	2	imp 277	1 |- ((ch /\ ph) -> ps)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  adantll 309  ad2antlr 321  ad2antrl 322  ad2antrr 323  jaao 330  sylan9 359  sylan9bb 418  im2anan9 434  im2anan9r 435  bi2bian9 480  pm5.18 497  ccase2 564  prlem1 576  sbcom 916  sbal1 996  mopick2 1057  2exeu 1066  2eu5 1071  cleqan12d 1116  sylan9eq 1144  eqvinc 1407  sylan9ss 1514  unss12 1630  elin 1635  copsex4g 1904  reuuni1 1955  solin 2145  wefrc 2195  ordelon 2222  tz7.7 2224  tfi 2244  ordunidif 2260  onint0 2262  onnmin 2270  onmindif 2312  onmindif2 2313  ordelsuc 2322  ordsucelsuc 2324  ordtri2or2 2329  ordsucun 2333  peano5 2394  findsg 2398  tfinds 2401  tfindsg 2402  ssnlim 2407  xp0r 2474  relssres 2596  imasn 2616  soirri 2629  elxp5 2641  imainss 2649  funssres 2698  funun 2700  fununi 2705  funcnvuni 2706  fco 2760  f1o2 2804  fnfvbr 2855  dmfco 2864  fvco 2865  fvopab3ig 2869  cleqfv 2880  fconst2 2902  f1ocnvfv1 2919  f1ocnvfv2 2920  isotr 2935  isotrALT 2936  isoini 2938  f1oiso 2942  tfrlem8 2956  tfrlem11 2959  tfr3 2964  rdglim2 2987  eloprabg 3035  oprabvalig 3048  oe0lem 3121  oe0 3130  oasuc 3131  omsuc 3133  oesuc 3134  oalim 3135  omlim 3136  oecl 3140  oawordri 3152  oaord1 3153  oaword2 3155  oawordeulem 3156  oaordex 3160  oa00 3161  oalimcl 3162  oaass 3163  nnarcl 3174  nndi 3180  nnmord 3189  omsmo 3196  ecoprass 3256  ecoprdi 3257  fundmen 3333  xpdom2 3345  pw2en 3348  sbthlem8 3356  sdomdomtr 3370  ensdomtr 3372  domsdomtr 3374  enen2 3376  domen1 3377  domen2 3378  mapenlem2 3385  mapxpen 3390  xpmapenlem5 3395  phplem3 3405  phplem5 3407  php2 3410  php3 3411  onomeneq 3414  onfin 3415  pssnn 3428  ssfi 3430  isfinite2 3437  unfilem1 3438  unfilem3 3440  zfregfr 3452  inf3lem6 3469  dfom3 3477  r1ord3 3501  r1val1 3502  tz9.12lem1 3503  rankr1 3518  r1pwcl 3530  aceq3 3556  ac6lem 3575  kmlem8 3587  zornlem3 3605  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodom 3613  fodomb 3615  carden 3638  carddom 3642  sucdom 3648  unxpdomlem 3649  cardlim 3657  cardiun 3665  alephcard 3673  alephnbtwn 3674  alephnbtwn2 3675  alephord 3680  alephsucdom 3685  cardaleph 3690  alephsson 3699  cflim 3704  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  addasspi 3817  mulasspi 3819  distrpi 3820  addnidpi 3822  ltapi 3824  ltmpi 3825  addcmpblnq 3846  addpipq 3848  addclpq 3852  addasspq 3857  distrpq 3861  ltaddpq 3873  ltexpq2 3875  halfpq 3876  ltbtwnpq 3878  prub 3892  genpnmax 3904  mulclprlem 3915  distrlem1pr 3921  distrlem2pr 3922  1idpr 3927  psslinpr 3929  prlem934b 3932  prlem934 3933  ltaddpr 3934  ltexprlem6 3941  ltexpri 3943  ltapr 3945  addcanpr 3946  prlem936 3949  reclem3pr 3952  reclem4pr 3953  suplem2pr 3956  mulgt0sr 4008  suppsr3 4018  axcnre 4087  subneg2t 4158  negdi2t 4201  divdivdivt 4265  divdiv23t 4271  letrt 4291  ltaddpost 4363  ledivt 4405  lt2sq 4414  peano2nn 4433  nn2get 4438  nnleltp1t 4448  nnaddm1clt 4452  sup2 4510  rimul 4534  nn0addclt 4551  nn0ltp1let 4556  nn0ltlem1 4558  elnnz1 4581  znegclt 4588  zltp1let 4597  zneo 4601  peano2uz 4602  uzind 4603  uzwo 4605  nnwoOLD 4608  zbtwnre 4619  flgzt 4626  qaddclt 4642  qmulclt 4644  om2uzlt 4654  seqrn 4673  expp1t 4678  sqr11 4761  sqrsq 4764  sqr2irr 4782  replimt 4798  facclt 4874  ruclem24 4908  ruclem27 4911  ruclem28 4912  nn0ennn 4925  xpnnen 4927  znnenlem 4929  znnen 4930  infxpidmlem4 4936  infxpidmlem5 4937  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem9 4941  infunabs 4946  infcdaabs 4947  infdif 4948  infmap2lem2 4952  hvsub4t 5014  hvsubcan1t 5016  normpyct 5093  hlimcaui 5141  helch 5151  occont 5168  ocorth 5172  occllem6 5185  occl 5188  projlem2 5194  projlem8 5200  projlem26 5218  pjthu 5241  pjthu2 5242  pjoml 5271  shsel1t 5286  hsupss 5310  spanss 5319  orthin 5371  chsscon2t 5419  chpsscon2t 5422  chdmm3t 5440  chdmm4t 5441  chdmj3t 5444  chdmj4t 5445  h1de2b 5459  elspansn2t 5472  spansncol 5473  spansnss2t 5480  spanunsn 5482  h1datom 5483  osumlem7 5536  5oalem1 5544  5oalem2 5545  5oalem3 5546  5oalem5 5548  pjot 5561  pjsumt 5590  pjadjco 5631  pjss1co 5633  pjss2co 5634  pjorthco 5639  pjscj 5640  pjclem4a 5652  pjclem4 5653  pjadj2co 5656  pj3s 5659  pj3cor1 5661  pjelt 5668  strlem3a 5693  stcltr1 5707  cvcon3t 5716  cvnbtwnt 5718  mdbr3 5729  mdbr4 5730  dmdbr 5731  ssmd2 5735  atn0 5743  atcveq0 5746  chrelat 5757  atcv0eq 5767  atcvatlem 5770  atcvat3 5774  atcvat4 5775  mdsymlem3 5778  mdsymlem4 5779  mdsymlem5 5780  sumdmdi 5785  sumdmdlem 5786  sumdmd 5787

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org