NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  anbi12d GIF version

Theorem anbi12d 691
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bi12d.1 (φ → (ψχ))
bi12d.2 (φ → (θτ))
Assertion
Ref Expression
anbi12d (φ → ((ψ θ) ↔ (χ τ)))

Proof of Theorem anbi12d
StepHypRef Expression
1 bi12d.1 . . 3 (φ → (ψχ))
21anbi1d 685 . 2 (φ → ((ψ θ) ↔ (χ θ)))
3 bi12d.2 . . 3 (φ → (θτ))
43anbi2d 684 . 2 (φ → ((χ θ) ↔ (χ τ)))
52, 4bitrd 244 1 (φ → ((ψ θ) ↔ (χ τ)))
Colors of variables: wff setvar class
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  2473  cbvreu  2833  cbvrexdva2  2840  cbvrab  2857  gencbvex  2901  rspce  2950  eqvincf  2967  ceqsrexv  2972  elrabf  2993  rexab2  3003  reu2  3024  reu6  3025  rmo4  3029  reu8  3032  reuind  3039  sbcan  3088  sbcang  3089  sbcabel  3123  rmob  3134  cbvreucsf  3200  cbvrabcsf  3201  psseq1  3356  psseq2  3357  ssconb  3399  pssdifcom1  3635  pssdifcom2  3636  2ralunsn  3880  elunii  3896  csbunig  3899  eluniab  3903  eluni1g  4172  opkelcokg  4261  opkelimagekg  4271  dfpw12  4301  sspw1  4335  reiota2  4368  dfnnc2  4395  eladdci  4399  addcid1  4405  peano5  4409  elsuc  4413  addcass  4415  nnsucelr  4428  opkltfing  4449  preaddccan2lem1  4454  preaddccan2  4455  ltfintr  4459  ssfin  4470  ncfinraise  4481  ncfinlower  4483  0ceven  4505  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  evenodddisjlem1  4515  eventfin  4517  oddtfin  4518  nnpweq  4523  sfin01  4528  sfindbl  4530  spfininduct  4540  1cvsfin  4542  vfinspsslem1  4550  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  opelopab2a  4702  setconslem4  4734  dfid3  4768  csbxpg  4813  vtoclr  4816  opeliunxp  4820  opeliunxp2  4822  opbrop  4841  elsnres  4996  dfres2  5002  elxp4  5108  nfunv  5138  fununi  5160  funcnvuni  5161  fneq1  5173  feq1  5210  f1eq1  5253  foeq1  5265  f1oeq1  5281  f1oeq2  5282  f1oeq3  5283  ffoss  5314  fv3  5341  dffn5  5363  fvopab3g  5386  fvopab3ig  5387  inpreima  5409  isoeq1  5482  isoeq4  5485  isoini  5497  f1oiso2  5500  fununiq  5517  cbvoprab1  5567  cbvoprab2  5568  cbvoprab12  5569  ov  5595  ovig  5597  ovg  5601  caovmo  5645  mpt2eq123dv  5663  cbvmpt  5676  cbvmpt2x  5678  ovmpt2x  5712  fmpt2x  5730  trtxp  5781  op1st2nd  5790  txpcofun  5803  fnfullfunlem1  5856  clos1conn  5879  clos1induct  5880  trd  5921  frd  5922  trrd  5925  antird  5928  antid  5929  frds  5935  bren  6030  endisj  6051  enprmapc  6083  mucnc  6131  ce0nnul  6177  ce2  6192  sbthlem2  6204  sbth  6206  lectr  6211  letc  6231  nmembers1lem1  6268  nmembers1lem3  6270  nchoicelem16  6304  nchoicelem17  6305  nchoicelem19  6307  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator