Theorem adantr 451

Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)

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 22	. 2 |- (ph -> (ch -> ps))
3	2	imp 418	1 |- ((ph /\ ch) -> ps)

Syntax hints:   -> wi 4   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  adantl  452  jaao  495  anim12ii  553  sylan9bb  680  ad2antrr  706  ad2antlr  707  ad2antrl  708  ad3antrrr  710  ad3antlr  711  ad4antr  712  ad4antlr  713  ad5antr  714  ad5antlr  715  ad6antr  716  ad6antlr  717  ad7antr  718  ad7antlr  719  ad8antr  720  ad8antlr  721  ad9antr  722  ad9antlr  723  ad10antr  724  ad10antlr  725  simp-4l  742  simp-4r  743  simp-5l  744  simp-5r  745  simp-6l  746  simp-6r  747  simp-7l  748  simp-7r  749  simp-8l  750  simp-8r  751  simp-9l  752  simp-9r  753  simp-10l  754  simp-10r  755  simp-11l  756  simp-11r  757  im2anan9  808  bi2bian9  845  ccase2  914  simpl1  958  simpl2  959  simpl3  960  3ad2ant1  976  3ad2ant2  977  simpll1  994  simpll2  995  simpll3  996  simplr1  997  simplr2  998  simplr3  999  simpl1l  1006  simpl1r  1007  simpl2l  1008  simpl2r  1009  simpl3l  1010  simpl3r  1011  simpl11  1030  simpl12  1031  simpl13  1032  simpl21  1033  simpl22  1034  simpl23  1035  simpl31  1036  simpl32  1037  simpl33  1038  cad1  1398  nfimdOLD  1809  ax12  1935  spimt  1974  sbequi  2059  nfsb4t  2080  dvelimdf  2082  sbcom  2089  ax12from12o  2156  ax11eq  2193  ax11el  2194  ax11indalem  2197  nfeud  2218  nfmod  2219  euan  2261  datisi  2313  fresison  2321  nfabd  2509  ralbid  2633  rexbid  2634  nfrald  2666  ralimdv  2694  ralcom2  2776  nfreud  2784  nfrmod  2785  reubidv  2796  rmobidv  2801  rabbidv  2852  elex22  2871  gencbvex  2902  rspct  2949  ceqsrexbv  2974  elrabf  2994  eueq3  3012  reu6  3026  reuind  3040  sbc2or  3055  sbcrext  3120  csbexg  3147  csbcomg  3160  csbiebt  3173  csbnestgOLD  3188  csbnest1gOLD  3190  sbcco3gOLD  3193  csbco3gOLD  3195  elin  3220  sseq1  3293  undif3  3516  difrab  3530  uneqdifeq  3639  diftpsn3  3850  eluni  3895  dfnfc2  3910  iuneq12d  3994  iuneq2d  3995  pwadjoin  4120  opkth1g  4131  elxpk  4197  opkabssvvk  4209  opkelopkabg  4246  opkelcokg  4262  opkelimagekg  4272  pw1equn  4332  pw1eqadj  4333  nfiotad  4343  findsd  4411  finds  4412  nnsucelr  4429  nndisjeq  4430  nnceleq  4431  nulge  4457  leltfintr  4459  ltfinp1  4463  lefinlteq  4464  ltfintri  4467  lenltfin  4470  ssfin  4471  ncfinsn  4477  ncfineleq  4478  ncfinraise  4482  ncfinlower  4484  tfin11  4494  tfinsuc  4499  tfinltfinlem1  4501  tfinltfin  4502  evennn  4507  oddnn  4508  sucevenodd  4511  sucoddeven  4512  evenodddisj  4517  nnadjoin  4521  sfindbl  4531  sfintfin  4533  sfinltfin  4536  sfin111  4537  vfinspnn  4542  vfintle  4547  vfinspsslem1  4551  vfinspss  4552  vinf  4556  phi11lem1  4596  nfopd  4606  copsexg  4608  elopab  4697  opeliunxp2  4823  ideqg  4869  brres  4950  dminss  5042  ssxpb  5056  xpcan  5058  xpcan2  5059  elxp4  5109  xpexr2  5111  funeu  5132  fununi  5161  funfni  5184  fco  5232  funssxp  5234  feu  5243  fimacnvdisj  5245  f1ss  5263  f1ores  5301  f1imacnv  5303  foimacnv  5304  fun11iun  5306  f1o00  5318  nffvd  5336  tz6.12-1  5345  fvelimab  5371  fvun  5379  eqfnfv  5393  fvimacnv  5404  ffvelrn  5416  dff3  5421  dffo3  5423  dffo4  5424  funiunfv  5468  f1ocnvfv1  5477  f1ofveu  5481  isocnv  5492  isotr  5496  isoini  5498  isoini2  5499  funsi  5521  oprabid  5551  eloprabga  5579  ov6g  5601  oprssov  5604  caovord3  5632  mpteq2dv  5669  cbvmpt2x  5679  fmpt2x  5731  composevalg  5818  fnpprod  5844  fnfullfunlem1  5857  clos10  5888  weds  5939  po0  5940  ersymb  5954  ertr  5955  erref  5960  erth  5969  qsdisj  5996  enadj  6061  enmap2lem3  6066  enprmaplem3  6079  nenpw1pwlem2  6086  brltc  6115  eqncg  6127  ncdisjun  6137  peano4nc  6151  eqtc  6162  pw1eltc  6163  tcdi  6165  ce0nnuli  6179  cenc  6182  lecidg  6197  lec0cg  6199  lecncvg  6200  sbthlem1  6204  sbthlem3  6206  leconnnc  6219  addceq0  6220  taddc  6230  tlecg  6231  ce2le  6234  cet  6235  nclenn  6250  addcdi  6251  muc0or  6253  lemuc1  6254  addccan2nc  6266  nmembers1lem3  6271  nmembers1  6272  nnc3n3p1  6279  spacind  6288  nchoicelem3  6292  nchoicelem4  6293  nchoicelem6  6295  nchoicelem7  6296  nchoicelem8  6297  nchoicelem9  6298  nchoicelem12  6301  nchoicelem14  6303  nchoicelem15  6304  nchoicelem17  6306  frecxp  6315  dmfrec  6317  fnfreclem3  6320  fnfrec  6321