Theorem anbi2d 619

Description: Deduction adding a left conjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
anbi2d	⊢ (φ → ((θ ⋀ ψ) ↔ (θ ⋀ χ)))

Proof of Theorem anbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 ⊢ (φ → (ψ ↔ χ))
2	1	biimpd 153	. . 3 ⊢ (φ → (ψ → χ))
3	2	anim2d 564	. 2 ⊢ (φ → ((θ ⋀ ψ) → (θ ⋀ χ)))
4	1	biimprd 154	. . 3 ⊢ (φ → (χ → ψ))
5	4	anim2d 564	. 2 ⊢ (φ → ((θ ⋀ χ) → (θ ⋀ ψ)))
6	3, 5	impbid 519	1 ⊢ (φ → ((θ ⋀ ψ) ↔ (θ ⋀ χ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  anbi1d 620  bibi2d 621  anbi12d 631  bi2anan9 635  2eu6 1459  eleq2 1542  ceqsex2 1843  eqvinc 1890  ceqsrex2v 1897  moeq3 1928  moi2 1931  moi 1932  sbc5g 1961  difeq2 2165  undif4 2337  r19.27zv 2365  prssg 2486  unieq 2524  intab 2574  opabbid 2684  opthg 2804  opthgg 2805  opelopab2 2835  pocl 2860  so 2880  ordelord 2986  dflim4 3135  xpeq2 3217  vtoclr 3227  opelxpg 3232  brinxp2 3247  opbrop 3254  coeq1 3297  opelco 3304  opelcog 3306  iss 3413  elxp4 3469  elxp5 3470  xp11 3492  fununi 3579  fneq2 3599  fneu 3608  fnun 3610  feq3 3638  fcoi1 3661  foeq3 3686  funbrfv 3766  fnopabfv 3774  ssimaexg 3785  fvco 3790  fvopab3 3793  fvopab3ig 3794  fvelrn 3828  elunirnALT 3885  isoeq2 3904  isoeq3 3905  isoini 3916  f1oiso 3920  tfrlem1 3927  tz7.44-1 3944  tz7.44-2 3945  tz7.44-3 3946  rdgeq1 3950  rdgeq2 3951  oprabbid 4011  cbvoprab3v 4016  fnoprval 4033  oprabval 4039  oprabvalig 4040  oprabval2gf 4042  oprabval3 4046  oprabval6g 4048  2ndconst 4113  ertr 4290  elqsiOLD 4309  brecop 4324  ecopoprtrn 4329  th3qlem1 4332  th3qlem2 4333  th3q 4335  pmvalg 4349  domeng 4398  dom2d 4422  xpassen 4460  xpdom2 4461  pw2en 4465  mapxpen 4515  unfilem3 4568  fiint 4575  inf0 4623  scott0 4734  aceq1 4746  aceq0 4747  aceq2 4748  aceq3lem 4749  aceq3 4750  aceq5lem1 4752  aceq6b 4759  axac 4762  ac6 4772  kmlem8 4789  kmlem14 4795  brdom7disj 4821  unxpdom 4864  iscard2 4874  cfval 4926  axrepndlem1 4964  axunndlem1 4967  axregnd 4976  axinfndlem1 4977  axacndlem4 4982  axacndlem5 4983  zfcndac 4991  ltsopq 5095  prcdpq 5117  prnmax 5119  genpv 5122  genpelv 5123  genpprecl 5124  genpnnp 5128  genpnmax 5130  distrlem1pr 5147  ltprord 5154  ltexprlem3 5164  ltexprlem4 5165  ltexpri 5169  reclem2pr 5177  ltsosr 5223  mulgt0sr 5234  map2psrpr 5240  suppsr 5242  supsrlem6 5250  ltresr 5278  supre 5280  ltsor 5281  pre-axmulgt0 5310  ltxr 5515  eqlelt 5539  lt2add 5663  le2add 5664  addgt0 5667  addgegt0 5668  addge0 5670  lesub0 5698  mulge0 5699  prodgt0 5838  prodge0 5840  ltrec 5898  lerec 5899  lt2msq 5900  le2msq 5917  sup3 6084  infm3 6086  infmsup 6100  supxrre 6115  prime 6230  uzwo4OLD 6245  zbtwnre 6256  qbtwnxr 6281  iooval 6333  iocval 6342  icoval 6343  iccval 6344  icoun 6381  uzwo 6423  uzwoOLD 6424  fzval 6437  elfzlem 6441  seq1vali 6513  ser1add2i 6539  ser1addi 6540  shftfvali 6543  sq11 6660  nn0opth2 6700  sqrval 6703  sqrle 6745  cru 6770  cj11 6862  abssubne0 6914  abs3lem 6939  cau3iri 6947  facwordi 6976  bcval 6990  clim 7009  fsumspli 7052  csbfsum 7059  fsumcom 7060  fsumrev 7061  fsummulc1 7065  clmi1i 7118  clm4ati 7122  climconst3 7128  climunii 7131  climaddlem3 7148  climmullem8 7159  climmulc2i 7161  iserzcmp0i 7175  cvgcmp3cetlem1 7220  cvgcmp3cetlem2 7221  cvgcmp3ceti 7222  geolim 7269  geolim1 7271  efseq1ex 7338  efaddlem24 7393  eftlexti 7410  ef1tlubi 7414  ef01tlubi 7418  absef01tlubi 7420  ef4p 7432  sinbnd 7498  cosbnd 7499  acdc3 7520  acdc2 7523  acdc5 7526  acdc 7528  ruclem12 7554  infxpidmlem2 7586  infmap2lem1 7612  infmap2 7614  eltopsp 7636  tpsex 7637  istps 7638  basis2 7645  eltg2 7649  eltg3 7656  tgss2 7667  basgen2 7669  neival 7743  isnei 7744  isneip 7746  cnpfval 7783  iscnp 7786  iscnp2 7787  cnpimaex 7791  cncnplem4 7803  ismet 7824  dfms2 7825  ismsg 7826  msflem 7829  metreslem 7848  blfval 7861  blelrn 7874  isopn 7885  metcnp 7913  metcnp2 7914  metcnpi 7916  metcnpi2 7917  metcni 7920  metcnss 7924  cncfmet 7931  tgioo 7941  lmbr 7954  lmbrf 7956  lmcvg 7958  iscau3 7964  iscau4 7966  metcn4i 7998  fsumcnlem 8015  lmcau 8022  bcthlem15 8039  isgrp 8067  isgrp2i 8101  grplactfval 8121  isring 8166  ringi 8167  vci 8192  isvclem 8221  nvcni 8354  nvcni2 8355  nvcni3 8356  va1cnlem 8370  sm1cnilem 8372  nvcnpi3 8447  nvcnpi4 8448  nmofval 8450  nmoval 8451  nmosetn0 8453  nmolb 8459  nmoubi 8460  nmo0 8476  nmlno0lem 8478  isphg 8501  htthlem3 8647  spwval2 8678  spwval 8684  spwnex 8686  sincosq3sgn 8730  efifolem3 8748  norm3lemt 9043  hlimi 9080  hlim2 9084  chlimi 9128  hlimcauii 9130  hlimunii 9133  ocsh 9180  occllem8 9204  projlem7 9216  projlem20 9229  pjmval 9262  shlub 9378  hosmval 9535  hommval 9536  hodmval 9537  hfsmval 9538  hfmmval 9539  cmbr 9551  spansncv 9622  eigorth 9788  nmopval 9806  elcnop 9807  nmopsetn0 9816  nmfnval 9827  nmfnsetn0 9829  elcnfn 9833  eigvecval 9846  nmoplb 9855  nmopub 9856  cnopc 9861  nmfnlb 9872  nmfnleub 9873  cnfnc 9878  braval 9891  kbval 9900  nmopnegi 9913  nmop0 9934  nmfn0 9935  nmlnop0iALT 9944  nmopun 9963  nmcopexlem1 9975  nmcfnexlem1 10004  branmfn 10062  leopmuli 10090  pjnmopi 10099  cvbr 10234  mdbr 10246  dmdbr 10251  atom1d 10305  chrelat2 10322  atcvati 10338  atord 10340  atcvat2 10341  irredlem4 10345  mdsymlem5 10359  cayleylem2 10435  vri 10522  bsi 10528  iseuctopg 10535  hmeogrp 10571  fillsb 10593  ismgra 10663  isalg 10674  algi 10681  isded 10690  dedi 10691  cmpasso 10727

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 147  df-an 225

Copyright terms: Public domain