Theorem adantr 306

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

Hypothesis

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

Assertion

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

Proof of Theorem adantr

Step	Hyp	Ref	Expression
1		adantr.1	. . 3 |- (ph -> ps)
2	1	a1d 14	. 2 |- (ph -> (ch -> ps))
3	2	imp 277	1 |- ((ph /\ ch) -> ps)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  adantlr 310  ad2antll 320  ad2antlr 321  ad2antrl 322  jaao 330  sylan9 359  anabsi5 377  sylan9bb 418  im2anan9 434  im2anan9r 435  bi2bian9 480  pm5.18 497  ccase2 564  prlem1 576  a4c1 844  sbequi 876  ddelimdf 909  cleqan12d 1116  sylan9eq 1144  birald 1217  birexd 1218  r19.20sdv 1257  bireudv 1318  elrabf 1421  sbc2or 1454  eldif 1496  sylan9ss 1514  pssn2lp 1571  unss12 1630  difrab 1695  copsexg 1902  eluni 1922  elopab 2110  itlso 2151  wefrc 2195  ordelord 2221  tz7.7 2224  ordunidif 2260  oneqmin 2273  ordsssuc 2310  onmindif2 2313  ordsucss 2320  ordelsuc 2322  ordsucelsuc 2324  ordsucsssuc 2325  suc11 2341  onuninsuc 2356  limsssuc 2362  limom 2387  nnsuc 2389  peano5 2394  tfindsg2 2403  ssnlim 2407  opelxpex 2445  opelxp 2452  weinxp 2467  xpex 2488  elxp5 2641  funun 2700  fununi 2705  funcnvuni 2706  resfunexg 2717  funfni 2724  fnssres 2734  fss 2759  fco 2760  feu 2767  f1o5 2808  f1ores 2813  f1imacnv 2814  f1o00 2823  tz6.12-1 2842  fnsnfv 2861  cleqfv 2880  ffvrn 2890  fopab2 2891  f1ocnvfv1 2919  f1ocnvfv2 2920  isocnv 2934  isotr 2935  isotrALT 2936  isoini 2938  isofrlem 2939  tfrlem2 2950  tfrlem4 2952  tfrlem8 2956  tfr3 2964  tz7.48-2 2995  tz7.49 2997  abianfplem 2999  eloprabg 3035  caoprord3 3072  f1stres 3096  oe0lem 3121  oevn0 3123  oecl 3140  om1r 3145  oaordi 3148  oawordri 3152  oaword1 3154  oawordex 3159  oaordex 3160  oa00 3161  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  nnarcl 3174  nnmord 3189  nnmcan 3190  omsmolem 3195  omsmo 3196  ecoprass 3256  dom2d 3307  fundmen 3333  xpsnen 3339  xpdom2 3345  sbthlem8 3356  mapenlem1 3384  mapxpen 3390  xpmapenlem3 3393  xpmapenlem5 3395  ssenen 3399  phplem3 3405  nneneq 3408  php3 3411  onomeneq 3414  nndomo 3416  finsucdom 3421  pssnn 3428  ssnn 3429  unblem4 3434  unbnn 3435  unfi2 3442  fiint 3445  inf3lem2 3465  inf3lem3 3466  inf3lem5 3468  trcl 3489  r1tr 3498  r1ord 3499  tz9.12lem3 3505  rankr1 3518  aceq5 3563  ac6lem 3575  kmlem12 3591  zornlem2 3604  zornlem7 3609  fodom 3613  fodomb 3615  carden 3638  carddom 3642  sucdom 3648  unxpdomlem 3649  sdomel 3653  ondomcard 3663  cardiun 3665  alephcard 3673  alephord 3680  alephsucdom 3685  cardaleph 3690  cflim 3704  cardcf 3706  cfsuc 3709  axextnd 3737  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  addasspi 3817  mulasspi 3819  mulcanpi 3821  ltexpi 3823  ltapi 3824  ltmpi 3825  indpi 3828  ltmpq 3871  ltexpq 3874  halfpq 3876  ltrpq 3879  prub 3892  genpcd 3903  genpnmax 3904  addclprlem1 3912  mulclprlem 3915  prlem934b 3932  prlem934 3933  ltaddpr 3934  ltexprlem5 3940  ltexprlem7 3942  ltapr 3945  prlem936a 3947  prlem936b 3948  reclem2pr 3951  reclem4pr 3953  ltasr 4003  recexsrlem 4006  suppsrlem 4015  suppsr2 4017  suppsr3 4018  supsrlem2 4020  suprelem 4053  axltadd 4085  axsup 4088  addcan 4120  mulcan 4207  div23t 4240  divmuldivt 4263  divdivdivt 4265  recdivt 4270  divdiv23t 4271  leltnet 4287  letrt 4291  ltnegcon1t 4367  lenegcon1t 4369  ledivt 4405  ltmuldiv2t 4407  ltdivmult 4408  lt2sq 4414  nnmulclt 4437  nn2get 4438  nnleltp1t 4448  nnaddm1clt 4452  nndiv 4453  sup2 4510  suprub 4513  nnreclt 4522  nn0addclt 4551  nn0ltp1let 4556  elnnz1 4581  zaddclt 4590  zrevaddclt 4592  znnsubt 4595  zltp1let 4597  zlem1ltt 4599  sqznn 4600  uzind 4603  uzwo 4605  nnwoOLD 4608  nn0ind 4612  zmax 4618  rebtwnz 4620  qaddclt 4642  qmulclt 4644  qrecclt 4646  qrevaddclt 4648  qbtwnre 4650  om2uzran 4655  expcllem 4682  expaddt 4698  le2sqet 4707  discrlem3 4715  nn0opthlem2 4723  sqrlem12 4742  sqrsq 4764  sqr2irr 4782  znnenlem 4929  znnen 4930  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infxpidmlem12 4944  infdif 4948  alephexp1 4954  hvm1negt 5007  hvsubcan1t 5016  his6 5057  normgt0t 5078  normpyct 5093  hcauchy 5103  shex 5115  closedsub 5128  chlim 5139  hlimcaui 5141  ch2 5149  occllem6 5185  projlem25 5217  projlem26 5218  pjthlem10 5234  pjthlem11 5235  pjvalt 5246  pjhclt 5248  hsupss 5310  spanss 5319  shlej2t 5357  chsscon1t 5418  chpsscon1t 5421  chdmm2t 5439  chdmj2t 5443  h1de2b 5459  spansncol 5473  spansneleq 5475  spansnss2t 5480  h1datom 5483  osumlem4 5533  osumlem6 5535  spansncv 5542  5oalem1 5544  5oalem2 5545  5oalem3 5546  5oalem5 5548  5oalem6 5549  3oalem1 5552  3oalem2 5553  pjjs 5585  pjv 5589  pjadjco 5631  pjnormss 5638  pjclem4 5653  pjadj2co 5656  pj3lem1 5658  pj3s 5659  stle 5681  stles 5682  stadd 5687  stadd3 5689  strlem3a 5693  strlem5 5696  jplem1 5701  stcltrlem1 5709  mdbr2 5728  dmdbr 5731  dmdbr2 5733  ssmd2 5735  atcveq0 5746  h1dat 5747  shatomic 5753  hatomistic 5755  cvexchlem 5759  atcv0eq 5767  atexch 5769  atcvatlem 5770  atcvat3 5774  atcvat4 5775  mdsymlem1 5776  mdsymlem2 5777  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdi 5785  sumdmdlem 5786

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