Theorem adantl 452

Description: Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Hypothesis

Ref	Expression
adantl.1	⊢ (φ → ψ)

Assertion

Ref	Expression
adantl	⊢ ((χ ∧ φ) → ψ)

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantl.1	. . 3 ⊢ (φ → ψ)
2	1	adantr 451	. 2 ⊢ ((φ ∧ χ) → ψ)
3	2	ancoms 439	1 ⊢ ((χ ∧ φ) → ψ)

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:  sylan2  460  jaao  495  anim12ii  553  sylan9bb  680  ad2antrl  708  ad2antll  709  im2anan9  808  bi2bian9  845  pm5.54  870  ccase2  914  rnlem  931  simpr1  961  simpr2  962  simpr3  963  3ad2ant3  978  simprl1  1000  simprl2  1001  simprl3  1002  simprr1  1003  simprr2  1004  simprr3  1005  simpr1l  1012  simpr1r  1013  simpr2l  1014  simpr2r  1015  simpr3l  1016  simpr3r  1017  simpr11  1039  simpr12  1040  simpr13  1041  simpr21  1042  simpr22  1043  simpr23  1044  simpr31  1045  simpr32  1046  simpr33  1047  falimd  1329  nfimdOLD  1809  spimt  1974  ax11v2  1992  ax11b  1995  nfsb4t  2080  sbcom  2089  sbal1  2126  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  2eu5  2288  dimatis  2320  nfrald  2666  nfreud  2784  nfrmod  2785  nfrmo  2787  nfrab  2793  gencbvex  2902  euind  3024  reu6  3026  reuind  3040  sbcan  3089  sbcralt  3119  sbcrext  3120  csbcomg  3160  csbiebt  3173  sbcnestgf  3184  sseq1  3293  undif3  3516  uneqdifeq  3639  ifeq1da  3688  ifeq2da  3689  ifclda  3690  ifbothda  3693  diftpsn3  3850  unissel  3921  unissint  3951  uniintsn  3964  pwadjoin  4120  opkelopkabg  4246  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  dfpw12  4302  pw1equn  4332  pw1eqadj  4333  nfiotad  4343  iota5  4360  iota2  4368  eladdc  4399  peano2  4404  nndisjeq  4430  nnceleq  4431  lefinaddc  4451  prepeano4  4452  preaddccan2  4456  ltfinirr  4458  ltfintr  4460  lefinlteq  4464  ltfintri  4467  ltlefin  4469  ssfin  4471  ncfinsn  4477  tfinprop  4490  tfinnnul  4491  tfin11  4494  tfindi  4497  tfinltfinlem1  4501  evenodddisj  4517  nnadjoin  4521  nnpweq  4524  sfintfin  4533  sfinltfin  4536  sfin111  4537  vfinspnn  4542  vfinspclt  4553  vinf  4556  nulnnn  4557  nfopd  4606  copsex2t  4609  opeliunxp  4821  ideqg  4869  ideqg2  4870  ssxpb  5056  xpcan  5058  xpcan2  5059  dfco2a  5082  xpexr2  5111  dfxp2  5114  funeu  5132  funssres  5145  fununi  5161  fnbr  5186  fco  5232  funssxp  5234  fssres2  5240  f1orescnv  5302  nffvd  5336  eqfnfv  5393  funfvbrb  5402  respreima  5411  fnasrn  5418  dff3  5421  ffvresb  5432  fconst5  5456  f1ocnvfv1  5477  isotr  5496  f1oiso  5500  funsi  5521  eloprabga  5579  ovg  5602  oprssov  5604  caovcl  5624  fvmpti  5700  fvmptss  5706  brtxp  5784  composevalg  5818  fnpprod  5844  fvfullfunlem3  5864  clos1conn  5880  po0  5940  erdisj  5973  ectocl  5993  xpsnen2g  6055  enadj  6061  enmap2lem3  6066  enmap2lem5  6068  enmap1lem5  6074  enprmaplem5  6081  nenpw1pwlem2  6086  eqncg  6127  ncdisjun  6137  1cnc  6140  ncssfin  6152  pw1eltc  6163  tcdi  6165  ce0nnul  6178  ce0nnuli  6179  cenc  6182  ce0  6191  lecidg  6197  lec0cg  6199  lecncvg  6200  addlec  6209  lecponc  6214  leconnnc  6219  addceq0  6220  dflec3  6222  ce2le  6234  cet  6235  nclenn  6250  addcdi  6251  muc0or  6253  addccan2nclem1  6264  ncslesuc  6268  nnc3n3p1  6279  spacind  6288  spacis  6289  nchoicelem8  6297  nchoicelem9  6298  nchoicelem12  6301  nchoicelem17  6306  frecxp  6315  fnfreclem3  6320  fnfrec  6321