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  522  pm5.17dc  794  orbididc  844  3anbi123d  1190  xorbi2d  1253  xorbi1d  1254  drsb1  1656  mopick  1954  clelab  2138  cbvrexf  2500  cbvreu  2503  cbvrexdva2  2510  cbvrab  2527  gencbvex  2571  rspce  2622  eqvincf  2640  ceqsrexv  2645  elrabf  2667  rexab2  2678  reu2  2700  reu6  2701  rmo4  2705  reu8  2708  reuind  2715  sbcan  2776  sbcang  2777  sbcabel  2810  rmob  2821  cbvrexcsf  2880  cbvreucsf  2881  cbvrabcsf  2882  difjust  2890  injust  2894  eldif  2898  psseq1  3002  psseq2  3003  ssconb  3047  elin  3097  opeq1  3515  opeq2  3516  2ralunsn  3535  elunii  3551  csbunig  3554  eluniab  3558  cbvopab  3794  cbvopab1  3796  cbvopab2  3797  cbvopab1s  3798  cbvopab2v  3800  cbvmpt  3817  trel  3827  nalset  3853  elssabg  3868  mss  3928  exss  3929  opelopab2a  3968  poeq1  4002  pocl  4006  soeq1  4018  ordeq  4050  zfun  4112  snnex  4122  reusv3  4133  regexmid  4194  peano5  4239  limom  4254  nnregexmid  4260  vtoclr  4306  opeliunxp  4313  poinxp  4327  opbrop  4337  csbxpg  4339  opeliunxp2  4394  relop  4404  brcogw  4422  elrnmpt1  4503  elsnres  4565  dfres2  4576  inimasn  4659  xpcanm  4678  xpcan2m  4679  elxp4  4726  elxp5  4727  cnvsom  4779  sbcfung  4842  funopg  4851  fununi  4884  funcnvuni  4885  fneq1  4904  2elresin  4927  feq1  4947  sbcfng  4961  sbcfg  4962  f1eq1  5003  foeq1  5018  f1oeq1  5033  f1oeq2  5034  f1oeq3  5035  ffoss  5074  brprcneu  5087  fv3  5113  tz6.12f  5118  ssimaex  5150  fvopab3g  5161  fvopab3ig  5162  fvopab6  5180  fmptco  5246  elunirn  5321  f1imaeq  5330  f1imapss  5331  foeqcnvco  5346  fliftfun  5352  fliftval  5356  isoeq1  5357  isoeq4  5360  isoini  5373  isopolem  5377  f1oiso2  5382  riotabidv  5386  cbvriota  5393  acexmid  5426  cbvoprab1  5490  cbvoprab2  5491  cbvoprab12  5492  cbvmpt2x  5496  ov  5534  ovig  5536  ovg  5553  caovimo  5608  caoftrn  5650  opabex3d  5662  opabex3  5663  elxp6  5710  unielxp  5714  dfoprab4  5732  dfoprab4f  5733  fmpt2x  5740  xporderlem  5765  poxp  5766  sprmpt2  5770  isprmpt2  5771  dftpos4  5791  tpostpos  5792  smoiso  5830  tfrlem3ag  5837  tfrlem3a  5838  tfrlemisucaccv  5851  tfrlemiex  5857  tfrlemi1  5858  tfrlemi14d  5859  tfrlemi14  5860  tfrexlem  5861  frec0g  5893  frecsuclem3  5897  frecsuc  5898  nnacan  5987  nnmcan  5994  nnaordex  6002  ertr  6023  brecop  6098  eroveu  6099  ecopovtrn  6105  ecopovtrng  6108  th3qlem1  6110  th3qlem2  6111  th3q  6113  ltsopi  6169  recexnq  6238  recmulnqg  6239  ltsonq  6246  lt2addnq  6252  ltbtwnnqq  6261  prarloclemarch2  6265  enq0sym  6276  enq0ref  6277  enq0tr  6278  enq0breq  6280  addnq0mo  6291  mulnq0mo  6292  addnnnq0  6293  mulnnnq0  6294  nqnq0a  6298  nqnq0m  6299  elinp  6317  prcdnql  6327  prcunqu  6328  prltlu  6330  prdisj  6335  prarloclemlo  6337  prarloclem3  6340  prarloclem5  6343  ltdfpr  6349  genprndl  6365  genprndu  6366  genpdisj  6367  appdivnq  6396  ltpopr  6421  ltexprlemdisj  6432  ltexprlemloc  6433  ltexprlemrl  6436  ltexprlemru  6438  ltexpri  6439  recexprlemm  6448  recexprlemdisj  6454  recexprlemloc  6455  recexprlem1ssl  6457  recexprlem1ssu  6458  recexpr  6462  aptiprleml  6463  addsrmo  6484  mulsrmo  6485  addsrpr  6486  mulsrpr  6487  lttrsr  6503  recexgt0sr  6514  ltresr  6548  axprecex  6572  axcnre  6573  axpre-lttrn  6576  axlttrn  6691  letri3  6702  letr  6704  le2add  7040  lt2add  7041  ltleadd  7042  lt2sub  7056  le2sub  7057  apreap  7177  apreim  7193  apti  7212  msq11  7454  cju  7499  peano5nni  7503  1nn  7511  peano2nn  7512  nn2ge  7532  nominpos  7743  dfuzi  7916  uzind  7917  xrletri3  8200  xrletr  8203  z2ge  8218  elixx1  8245  elioo2  8269  iooshf  8300  iooneg  8335  iccneg  8336  icoshft  8337  bj-sseq  8388  bj-nalset  8468  bj-indeq  8506  bj-2inf  8514  peano5set  8516
  Copyright terms: Public domain W3C validator