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

Theorem anbi12d 445
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 441 . 2 (φ → ((ψ θ) ↔ (χ θ)))
3 anbi12d.2 . . 3 (φ → (θτ))
43anbi2d 440 . 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  525  pm5.17dc  803  orbididc  848  3anbi123d  1192  xorbi2d  1255  xorbi1d  1256  drsb1  1662  mopick  1960  clelab  2144  cbvrexf  2506  cbvreu  2509  cbvrexdva2  2516  cbvrab  2533  gencbvex  2577  rspce  2628  eqvincf  2646  ceqsrexv  2651  elrabf  2673  rexab2  2684  reu2  2706  reu6  2707  rmo4  2711  reu8  2714  reuind  2721  sbcan  2782  sbcang  2783  sbcabel  2816  rmob  2827  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  difjust  2896  injust  2900  eldif  2904  psseq1  3008  psseq2  3009  ssconb  3053  elin  3103  opeq1  3523  opeq2  3524  2ralunsn  3543  elunii  3559  csbunig  3562  eluniab  3566  cbvopab  3802  cbvopab1  3804  cbvopab2  3805  cbvopab1s  3806  cbvopab2v  3808  cbvmpt  3825  trel  3835  nalset  3861  elssabg  3876  mss  3936  exss  3937  opelopab2a  3976  poeq1  4010  pocl  4014  soeq1  4026  ordeq  4058  zfun  4121  snnex  4131  reusv3  4142  regexmid  4203  peano5  4248  limom  4263  nnregexmid  4269  vtoclr  4315  opeliunxp  4322  poinxp  4336  opbrop  4346  csbxpg  4348  opeliunxp2  4403  relop  4413  brcogw  4431  elrnmpt1  4512  elsnres  4574  dfres2  4585  inimasn  4668  xpcanm  4687  xpcan2m  4688  elxp4  4735  elxp5  4736  cnvsom  4788  sbcfung  4851  funopg  4860  fununi  4893  funcnvuni  4894  fneq1  4913  2elresin  4936  feq1  4956  sbcfng  4970  sbcfg  4971  f1eq1  5012  foeq1  5027  f1oeq1  5042  f1oeq2  5043  f1oeq3  5044  ffoss  5083  brprcneu  5096  fv3  5122  tz6.12f  5127  ssimaex  5159  fvopab3g  5170  fvopab3ig  5171  fvopab6  5189  fmptco  5255  elunirn  5330  f1imaeq  5339  f1imapss  5340  foeqcnvco  5355  fliftfun  5361  fliftval  5365  isoeq1  5366  isoeq4  5369  isoini  5382  isopolem  5386  f1oiso2  5391  riotabidv  5395  cbvriota  5402  acexmid  5435  cbvoprab1  5499  cbvoprab2  5500  cbvoprab12  5501  cbvmpt2x  5505  ov  5543  ovig  5545  ovg  5562  caovimo  5617  caoftrn  5659  opabex3d  5671  opabex3  5672  elxp6  5719  unielxp  5723  dfoprab4  5741  dfoprab4f  5742  fmpt2x  5749  xporderlem  5774  poxp  5775  sprmpt2  5779  isprmpt2  5780  dftpos4  5800  tpostpos  5801  smoiso  5839  tfrlem3ag  5846  tfrlem3a  5847  tfrlemisucaccv  5860  tfrlemiex  5866  tfrlemi1  5867  tfrlemi14d  5868  tfrlemi14  5869  tfrexlem  5870  frec0g  5902  frecsuclem3  5906  frecsuc  5907  nnacan  5996  nnmcan  6003  nnaordex  6011  ertr  6032  brecop  6107  eroveu  6108  ecopovtrn  6114  ecopovtrng  6117  th3qlem1  6119  th3qlem2  6120  th3q  6122  ltsopi  6180  recex  6249  recmulnqg  6250  ltsonq  6257  lt2addnq  6263  ltbtwnnqq  6272  prarloclemarch2  6276  enq0sym  6287  enq0ref  6288  enq0tr  6289  enq0breq  6291  addnq0mo  6302  mulnq0mo  6303  addnnnq0  6304  mulnnnq0  6305  nqnq0a  6309  nqnq0m  6310  elinp  6328  prcdnql  6338  prcunqu  6339  prltlu  6341  prdisj  6346  prarloclemlo  6348  prarloclem3  6351  prarloclem5  6354  ltdfpr  6360  genprndl  6376  genprndu  6377  genpdisj  6378  appdivnq  6407  ltpopr  6432  ltexprlemdisj  6443  ltexprlemloc  6444  ltexprlemrl  6447  ltexprlemru  6449  ltexpri  6450  recexprlemm  6458  recexprlemdisj  6464  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468  recexpr  6472  addsrmo  6490  mulsrmo  6491  addsrpr  6492  mulsrpr  6493  lttrsr  6509  ltresr  6550  axcnre  6575  axpre-lttrn  6578  axlttrn  6689  letr  6699  bj-sseq  7038  bj-nalset  7118  bj-indeq  7152  bj-2inf  7160  peano5set  7162
  Copyright terms: Public domain W3C validator