Theorem anbi12d 691

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bi12d.1	|- (ph -> (ps <-> ch))
bi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
anbi12d	|- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Proof of Theorem anbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	anbi1d 685	. 2 |- (ph -> ((ps /\ th) <-> (ch /\ th)))
3		bi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	anbi2d 684	. 2 |- (ph -> ((ch /\ th) <-> (ch /\ ta)))
5	2, 4	bitrd 244	1 |- (ph -> ((ps /\ th) <-> (ch /\ ta)))

Syntax hints:   -> wi 4   <-> wb 176   /\ 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:  pm4.38  842  3anbi123d  1252  cadbi123d  1383  drsb1  2022  mopick  2266  clelab  2474  cbvreu  2834  cbvrexdva2  2841  cbvrab  2858  gencbvex  2902  rspce  2951  eqvincf  2968  ceqsrexv  2973  elrabf  2994  rexab2  3004  reu2  3025  reu6  3026  rmo4  3030  reu8  3033  reuind  3040  sbcan  3089  sbcang  3090  sbcabel  3124  rmob  3135  cbvreucsf  3201  cbvrabcsf  3202  psseq1  3357  psseq2  3358  ssconb  3400  pssdifcom1  3636  pssdifcom2  3637  2ralunsn  3881  elunii  3897  csbunig  3900  eluniab  3904  eluni1g  4173  opkelcokg  4262  opkelimagekg  4272  dfpw12  4302  sspw1  4336  reiota2  4369  dfnnc2  4396  eladdci  4400  addcid1  4406  peano5  4410  elsuc  4414  addcass  4416  nnsucelr  4429  opkltfing  4450  preaddccan2lem1  4455  preaddccan2  4456  ltfintr  4460  ssfin  4471  ncfinraise  4482  ncfinlower  4484  0ceven  4506  evennn  4507  oddnn  4508  evennnul  4509  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  evenodddisjlem1  4516  eventfin  4518  oddtfin  4519  nnpweq  4524  sfin01  4529  sfindbl  4531  spfininduct  4541  1cvsfin  4543  vfinspsslem1  4551  cbvopab  4631  cbvopab1  4633  cbvopab2  4634  cbvopab1s  4635  cbvopab2v  4637  opelopab2a  4703  setconslem4  4735  dfid3  4769  csbxpg  4814  vtoclr  4817  opeliunxp  4821  opeliunxp2  4823  opbrop  4842  elsnres  4997  dfres2  5003  elxp4  5109  nfunv  5139  fununi  5161  funcnvuni  5162  fneq1  5174  feq1  5211  f1eq1  5254  foeq1  5266  f1oeq1  5282  f1oeq2  5283  f1oeq3  5284  ffoss  5315  fv3  5342  dffn5  5364  fvopab3g  5387  fvopab3ig  5388  inpreima  5410  isoeq1  5483  isoeq4  5486  isoini  5498  f1oiso2  5501  fununiq  5518  cbvoprab1  5568  cbvoprab2  5569  cbvoprab12  5570  ov  5596  ovig  5598  ovg  5602  caovmo  5646  mpt2eq123dv  5664  cbvmpt  5677  cbvmpt2x  5679  ovmpt2x  5713  fmpt2x  5731  trtxp  5782  op1st2nd  5791  txpcofun  5804  fnfullfunlem1  5857  clos1conn  5880  clos1induct  5881  trd  5922  frd  5923  trrd  5926  antird  5929  antid  5930  frds  5936  bren  6031  endisj  6052  enprmapc  6084  mucnc  6132  ce0nnul  6178  ce2  6193  sbthlem2  6205  sbth  6207  lectr  6212  letc  6232  nmembers1lem1  6269  nmembers1lem3  6271  nchoicelem16  6305  nchoicelem17  6306  nchoicelem19  6308  fnfreclem3  6320  fnfrec  6321