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

Theorem imbi12d 232
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
imbi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21imbi1d 229 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43imbi2d 228 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 186 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfbidf  1473  drnf1  1662  drnf2  1663  equveli  1683  ax11v2  1742  ax11v  1749  ax11ev  1750  equs5or  1752  mobidh  1976  mobid  1977  axext3  2065  cbvralf  2572  cbvraldva2  2582  gencbval  2648  vtoclgaf  2664  vtocl2gaf  2666  vtocl3gaf  2668  rspct  2695  rspc  2696  rspc2gv  2713  ceqex  2723  ralab2  2757  mob2  2773  mob  2775  morex  2777  reu7  2788  reu8  2789  nelrdva  2798  cdeqim  2809  sbcimg  2856  csbhypf  2942  cbvralcsf  2965  dfss2f  2991  sbcssg  3352  sneqrg  3556  elintab  3649  intss1  3653  intmin  3658  dfiin2g  3713  trel  3884  trss  3886  bnd2  3949  zfpow  3951  rext  3972  opth  3994  copsexg  4001  poeq1  4056  pocl  4060  swopolem  4062  swopo  4063  soeq1  4072  sowlin  4077  frforeq2  4102  frforeq3  4104  frirrg  4107  frind  4109  weeq1  4113  ordelord  4138  reusv3i  4211  ordtriexmid  4267  ontr2exmid  4270  onsucsssucexmid  4272  onsucelsucexmid  4275  ordsucunielexmid  4276  regexmidlem1  4278  regexmid  4280  reg2exmid  4281  elirr  4286  en2lp  4299  ordsoexmid  4307  onintexmid  4317  reg3exmid  4324  tfis  4326  tfisi  4330  peano2  4338  findes  4346  nnregexmid  4362  vtoclr  4408  poinxp  4429  soinxp  4430  posng  4432  ssrel  4448  ssrel2  4450  ssrelrel  4460  relop  4508  issref  4731  iota5  4911  dffun4f  4942  sbcfung  4949  funopg  4958  brprcneu  5196  funfveu  5213  tz6.12f  5228  funbrfv  5238  ssimaexg  5261  fvmptss2  5273  fvmptssdm  5281  fvmptf  5289  fvelrn  5324  f1veqaeq  5434  dff13f  5435  isopolem  5486  isosolem  5488  riota5f  5517  oprabid  5562  ovmpt2s  5649  ov2gf  5650  ovi3  5662  caovcan  5690  caovordig  5691  caofrss  5760  caoftrn  5761  dfoprab4f  5844  f1o2ndf1  5874  poxp  5878  smoel  5943  tfrlem1  5951  tfr1onlemsucfn  5983  tfr1onlemsucaccv  5984  tfr1onlembxssdm  5986  tfr1onlembfn  5987  tfr1onlemaccex  5991  tfr1onlemres  5992  tfrcllemsucfn  5996  tfrcllemsucaccv  5997  tfrcllembxssdm  5999  tfrcllembfn  6000  tfrcllemaccex  6004  tfrcllemres  6005  tfrcl  6007  nnsucelsuc  6128  nnsucsssuc  6129  nnmordi  6148  nnaordex  6159  qsel  6242  eroveu  6256  ecopovtrn  6262  ecopovtrng  6265  th3qlem2  6268  fundmeng  6346  phplem3g  6381  nneneq  6382  ssfiexmid  6401  domfiexmid  6403  findcard  6412  findcard2  6413  findcard2s  6414  findcard2d  6415  findcard2sd  6416  diffifi  6418  ac6sfi  6421  supeq3  6452  supeq123d  6453  supmoti  6455  suplubti  6462  supisolem  6470  cnvinfex  6480  eqinfti  6482  infvalti  6484  ordiso2  6495  ltsonq  6639  ltexnqq  6649  prcdnql  6725  prcunqu  6726  prloc  6732  prdisj  6733  genprndl  6762  genprndu  6763  caucvgprlemnkj  6907  caucvgprlemnbj  6908  caucvgprlemcl  6917  caucvgprprlemcbv  6928  caucvgprprlemval  6929  lttrsr  6990  ltsosr  6992  recexgt0sr  7001  mulgt0sr  7005  aptisr  7006  mulextsr1  7008  srpospr  7010  caucvgsrlemgt1  7022  caucvgsrlemoffres  7027  caucvgsr  7029  axprecex  7097  axpre-ltwlin  7100  axpre-lttrn  7101  axpre-apti  7102  axpre-mulgt0  7104  axpre-mulext  7105  axcaucvglemcau  7115  axcaucvglemres  7116  ltleletr  7249  squeeze0  8038  nnsub  8133  fzind  8532  uzind4s  8748  uzind4s2  8749  indstr  8751  supinfneg  8753  infsupneg  8754  frec2uzuzd  9473  frec2uzltd  9474  uzsinds  9507  iseqfveq2  9533  iseqshft2  9537  monoord  9540  iseqsplit  9543  iseqid2  9553  expcl2lemap  9574  facdiv  9751  facwordi  9753  caucvgre  9994  fimaxre2  10236  climcn1  10274  climcn2  10275  subcn2  10277  ndvdssub  10463  bezoutlemmain  10520  bezoutlemex  10523  bezoutlemzz  10524  bezoutlemsup  10531  dfgcd2  10536  ialgcvg  10563  ialgcvga  10566  ialgfx  10567  lcmgcdlem  10592  lcmdvds  10594  coprmgcdb  10603  coprmdvds1  10606  coprmdvds2  10608  prmind2  10635  dvdsprime  10637  nprm  10638  dvdsprm  10651  exprmfct  10652  coprm  10656  isprm6  10659  prmfac1  10664  sqrt2irr  10674  cbvrald  10734  bj-bdfindes  10887  bj-omtrans  10894  bj-inf2vnlem1  10908  bj-inf2vnlem2  10909  bj-inf2vnlem3  10910  bj-inf2vnlem4  10911  bj-findes  10919  strcoll2  10921  sscoll2  10926
  Copyright terms: Public domain W3C validator