ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anbi12d 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  810  orbididc  860  3anbi123d  1207  xorbi2d  1271  xorbi1d  1272  drsb1  1680  mopick  1978  clelab  2162  cbvrexf  2525  cbvreu  2528  cbvrexdva2  2535  cbvrab  2552  gencbvex  2597  rspce  2648  eqvincf  2666  ceqsrexv  2671  elrabf  2693  rexab2  2704  reu2  2726  reu6  2727  rmo4  2731  reu8  2734  reuind  2741  sbcan  2802  sbcang  2803  sbcabel  2836  rmob  2847  cbvrexcsf  2906  cbvreucsf  2907  cbvrabcsf  2908  difjust  2916  injust  2920  eldif  2924  psseq1  3028  psseq2  3029  ssconb  3073  elin  3123  opeq1  3546  opeq2  3547  2ralunsn  3566  elunii  3582  csbunig  3585  eluniab  3589  cbvopab  3825  cbvopab1  3827  cbvopab2  3828  cbvopab1s  3829  cbvopab2v  3831  cbvmpt  3848  trel  3858  nalset  3884  elssabg  3899  mss  3959  exss  3960  opelopab2a  3999  poeq1  4033  pocl  4037  soeq1  4049  ordeq  4096  zfun  4158  snnex  4168  reusv3  4179  ontr2exmid  4237  regexmid  4246  peano5  4299  limom  4314  nnregexmid  4320  vtoclr  4366  opeliunxp  4373  poinxp  4387  opbrop  4397  csbxpg  4399  opeliunxp2  4454  relop  4464  brcogw  4482  elrnmpt1  4563  elsnres  4625  dfres2  4636  inimasn  4719  xpcanm  4738  xpcan2m  4739  elxp4  4786  elxp5  4787  cnvsom  4839  sbcfung  4903  funopg  4912  fununi  4945  funcnvuni  4946  fneq1  4965  2elresin  4988  feq1  5008  sbcfng  5022  sbcfg  5023  f1eq1  5065  foeq1  5080  f1oeq1  5095  f1oeq2  5096  f1oeq3  5097  ffoss  5136  brprcneu  5149  fv3  5175  tz6.12f  5180  ssimaex  5212  fvopab3g  5223  fvopab3ig  5224  fvopab6  5242  fmptco  5308  elunirn  5383  f1imaeq  5392  f1imapss  5393  foeqcnvco  5408  fliftfun  5414  fliftval  5418  isoeq1  5419  isoeq4  5422  isoini  5435  isopolem  5439  f1oiso2  5444  riotabidv  5448  cbvriota  5456  acexmid  5489  cbvoprab1  5554  cbvoprab2  5555  cbvoprab12  5556  cbvmpt2x  5560  ov  5598  ovig  5600  ovg  5617  caovimo  5672  caoftrn  5714  opabex3d  5726  opabex3  5727  elxp6  5774  unielxp  5778  dfoprab4  5796  dfoprab4f  5797  fmpt2x  5804  xporderlem  5830  poxp  5831  sprmpt2  5835  isprmpt2  5836  dftpos4  5856  tpostpos  5857  smoiso  5895  tfrlem3ag  5902  tfrlem3a  5903  tfr0  5915  tfrlemisucaccv  5917  tfrlemiex  5923  tfrlemi1  5924  tfrlemi14d  5925  tfrexlem  5926  frec0g  5961  frecsuclem3  5968  frecsuc  5969  nnacan  6063  nnmcan  6070  nnaordex  6078  ertr  6099  brecop  6174  eroveu  6175  ecopovtrn  6181  ecopovtrng  6184  th3qlem1  6186  th3qlem2  6187  th3q  6189  xpsnen  6273  endisj  6276  phplem3g  6297  ssfiexmid  6314  findcard2s  6324  ac6sfi  6329  ltsopi  6390  recexnq  6460  recmulnqg  6461  ltsonq  6468  lt2addnq  6474  lt2mulnq  6475  ltbtwnnqq  6485  prarloclemarch2  6489  enq0sym  6502  enq0ref  6503  enq0tr  6504  enq0breq  6506  addnq0mo  6517  mulnq0mo  6518  addnnnq0  6519  mulnnnq0  6520  nqnq0a  6524  nqnq0m  6525  elinp  6544  prcdnql  6554  prcunqu  6555  prltlu  6557  prdisj  6562  prarloclemlo  6564  prarloclem3  6567  prarloclem5  6570  ltdfpr  6576  genprndl  6591  genprndu  6592  genpdisj  6593  appdivnq  6633  ltpopr  6665  ltexprlemdisj  6676  ltexprlemloc  6677  ltexprlemrl  6680  ltexprlemru  6682  ltexpri  6683  recexprlemm  6694  recexprlemdisj  6700  recexprlemloc  6701  recexprlem1ssl  6703  recexprlem1ssu  6704  recexpr  6708  aptiprleml  6709  archpr  6713  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  cauappcvgprlem1  6729  cauappcvgprlemlim  6731  cauappcvgpr  6732  caucvgprlemnkj  6736  caucvgprlemnbj  6737  caucvgprlemcl  6746  caucvgpr  6752  caucvgprprlemcbv  6757  caucvgprprlemval  6758  caucvgprprlemopu  6769  caucvgprpr  6782  addsrmo  6800  mulsrmo  6801  addsrpr  6802  mulsrpr  6803  lttrsr  6819  recexgt0sr  6830  caucvgsrlemcau  6849  caucvgsrlemgt1  6851  caucvgsrlemoffcau  6854  caucvgsrlemoffres  6856  caucvgsr  6858  ltresr  6887  pitonn  6896  peano1nnnn  6900  peano2nnnn  6901  axprecex  6926  axcnre  6927  axpre-lttrn  6930  peano5nnnn  6938  axcaucvglemcau  6944  axcaucvglemres  6945  axlttrn  7059  letri3  7070  letr  7072  le2add  7408  lt2add  7409  ltleadd  7410  lt2sub  7424  le2sub  7425  apreap  7545  apreim  7561  apti  7580  msq11  7835  cju  7880  peano5nni  7884  1nn  7892  peano2nn  7893  nn2ge  7913  nominpos  8126  elz2  8275  dfuzi  8311  uzind  8312  xrletri3  8679  xrletr  8682  z2ge  8697  elixx1  8724  elioo2  8748  iooshf  8779  iooneg  8814  iccneg  8815  icoshft  8816  elfz1  8837  fzdifsuc  8901  fzrev  8904  1fv  8954  nnesq  9237  shftlem  9286  shftfibg  9290  shftfib  9293  shftfn  9294  2shfti  9301  cjval  9314  cjth  9315  remim  9329  caucvgrelemcau  9448  caucvgre  9449  cvg1nlemcau  9452  cvg1nlemres  9453  rexanuz2  9458  recvguniq  9462  resqrexlemgt0  9487  resqrexlemoverl  9488  resqrexlemglsq  9489  resqrexlemsqa  9491  resqrexlemex  9492  rsqrmo  9494  resqrtcl  9496  rersqrtthlem  9497  absdiflt  9557  absdifle  9558  cau3lem  9579  icodiamlt  9645  clim  9670  clim2  9672  climshftlemg  9691  addcn2  9699  climcau  9734  sumeq1  9742  bj-sseq  9795  bj-nalset  9879  bj-indeq  9917  bj-2inf  9926
  Copyright terms: Public domain W3C validator