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  6415  enq0ref  6416  enq0tr  6417  enq0breq  6419  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  mulnnnq0  6433  nqnq0a  6437  nqnq0m  6438  elinp  6457  prcdnql  6467  prcunqu  6468  prltlu  6470  prdisj  6475  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  ltdfpr  6489  genprndl  6504  genprndu  6505  genpdisj  6506  appdivnq  6544  ltpopr  6569  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  ltexpri  6587  recexprlemm  6596  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  recexpr  6610  aptiprleml  6611  archpr  6615  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  cauappcvgpr  6634  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemcl  6647  caucvgpr  6653  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  lttrsr  6690  recexgt0sr  6701  ltresr  6736  pitonn  6744  axprecex  6764  axcnre  6765  axpre-lttrn  6768  axlttrn  6885  letri3  6896  letr  6898  le2add  7234  lt2add  7235  ltleadd  7236  lt2sub  7250  le2sub  7251  apreap  7371  apreim  7387  apti  7406  msq11  7649  cju  7694  peano5nni  7698  1nn  7706  peano2nn  7707  nn2ge  7727  nominpos  7939  elz2  8088  dfuzi  8124  uzind  8125  xrletri3  8491  xrletr  8494  z2ge  8509  elixx1  8536  elioo2  8560  iooshf  8591  iooneg  8626  iccneg  8627  icoshft  8628  elfz1  8649  fzdifsuc  8713  fzrev  8716  1fv  8766  nnesq  9021  cjval  9073  cjth  9074  remim  9088  bj-sseq  9266  bj-nalset  9350  bj-indeq  9388  bj-2inf  9397
  Copyright terms: Public domain W3C validator