ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi12d Structured version   GIF version

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

Proof of Theorem anbi12d
StepHypRef Expression
1 anbi12d.1 . . 3 (φ → (ψχ))
21anbi1d 438 . 2 (φ → ((ψ θ) ↔ (χ θ)))
3 anbi12d.2 . . 3 (φ → (θτ))
43anbi2d 437 . 2 (φ → ((χ θ) ↔ (χ τ)))
52, 4bitrd 177 1 (φ → ((ψ θ) ↔ (χ τ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm4.38  537  pm5.17dc  809  orbididc  859  3anbi123d  1206  xorbi2d  1269  xorbi1d  1270  drsb1  1677  mopick  1975  clelab  2159  cbvrexf  2522  cbvreu  2525  cbvrexdva2  2532  cbvrab  2549  gencbvex  2594  rspce  2645  eqvincf  2663  ceqsrexv  2668  elrabf  2690  rexab2  2701  reu2  2723  reu6  2724  rmo4  2728  reu8  2731  reuind  2738  sbcan  2799  sbcang  2800  sbcabel  2833  rmob  2844  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  difjust  2913  injust  2917  eldif  2921  psseq1  3025  psseq2  3026  ssconb  3070  elin  3120  opeq1  3540  opeq2  3541  2ralunsn  3560  elunii  3576  csbunig  3579  eluniab  3583  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  cbvmpt  3842  trel  3852  nalset  3878  elssabg  3893  mss  3953  exss  3954  opelopab2a  3993  poeq1  4027  pocl  4031  soeq1  4043  ordeq  4075  zfun  4137  snnex  4147  reusv3  4158  regexmid  4219  peano5  4264  limom  4279  nnregexmid  4285  vtoclr  4331  opeliunxp  4338  poinxp  4352  opbrop  4362  csbxpg  4364  opeliunxp2  4419  relop  4429  brcogw  4447  elrnmpt1  4528  elsnres  4590  dfres2  4601  inimasn  4684  xpcanm  4703  xpcan2m  4704  elxp4  4751  elxp5  4752  cnvsom  4804  sbcfung  4868  funopg  4877  fununi  4910  funcnvuni  4911  fneq1  4930  2elresin  4953  feq1  4973  sbcfng  4987  sbcfg  4988  f1eq1  5030  foeq1  5045  f1oeq1  5060  f1oeq2  5061  f1oeq3  5062  ffoss  5101  brprcneu  5114  fv3  5140  tz6.12f  5145  ssimaex  5177  fvopab3g  5188  fvopab3ig  5189  fvopab6  5207  fmptco  5273  elunirn  5348  f1imaeq  5357  f1imapss  5358  foeqcnvco  5373  fliftfun  5379  fliftval  5383  isoeq1  5384  isoeq4  5387  isoini  5400  isopolem  5404  f1oiso2  5409  riotabidv  5413  cbvriota  5421  acexmid  5454  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvmpt2x  5524  ov  5562  ovig  5564  ovg  5581  caovimo  5636  caoftrn  5678  opabex3d  5690  opabex3  5691  elxp6  5738  unielxp  5742  dfoprab4  5760  dfoprab4f  5761  fmpt2x  5768  xporderlem  5793  poxp  5794  sprmpt2  5798  isprmpt2  5799  dftpos4  5819  tpostpos  5820  smoiso  5858  tfrlem3ag  5865  tfrlem3a  5866  tfr0  5878  tfrlemisucaccv  5880  tfrlemiex  5886  tfrlemi1  5887  tfrlemi14d  5888  tfrexlem  5889  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnacan  6021  nnmcan  6028  nnaordex  6036  ertr  6057  brecop  6132  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  th3qlem2  6145  th3q  6147  xpsnen  6231  endisj  6234  ssfiexmid  6254  ltsopi  6304  recexnq  6374  recmulnqg  6375  ltsonq  6382  lt2addnq  6388  ltbtwnnqq  6398  prarloclemarch2  6402  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  nqnq0a  6436  nqnq0m  6437  elinp  6456  prcdnql  6466  prcunqu  6467  prltlu  6469  prdisj  6474  prarloclemlo  6476  prarloclem3  6479  prarloclem5  6482  ltdfpr  6488  genprndl  6504  genprndu  6505  genpdisj  6506  appdivnq  6542  ltpopr  6567  ltexprlemdisj  6578  ltexprlemloc  6579  ltexprlemrl  6582  ltexprlemru  6584  ltexpri  6585  recexprlemm  6594  recexprlemdisj  6600  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  recexpr  6608  aptiprleml  6609  archpr  6613  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  lttrsr  6650  recexgt0sr  6661  ltresr  6696  pitonn  6704  axprecex  6724  axcnre  6725  axpre-lttrn  6728  axlttrn  6845  letri3  6856  letr  6858  le2add  7194  lt2add  7195  ltleadd  7196  lt2sub  7210  le2sub  7211  apreap  7331  apreim  7347  apti  7366  msq11  7609  cju  7654  peano5nni  7658  1nn  7666  peano2nn  7667  nn2ge  7687  nominpos  7899  elz2  8048  dfuzi  8084  uzind  8085  xrletri3  8451  xrletr  8454  z2ge  8469  elixx1  8496  elioo2  8520  iooshf  8551  iooneg  8586  iccneg  8587  icoshft  8588  elfz1  8609  fzdifsuc  8673  fzrev  8676  1fv  8726  nnesq  8981  cjval  9033  cjth  9034  remim  9048  bj-sseq  9200  bj-nalset  9280  bj-indeq  9318  bj-2inf  9326  peano5set  9328
  Copyright terms: Public domain W3C validator