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

Theorem imbi12d 233
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 230 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43imbi2d 229 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 187 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  stbid  817  nfbidf  1519  drnf1  1711  drnf2  1712  equveli  1732  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  mobidh  2031  mobid  2032  axext3  2120  cbvralf  2646  cbvraldva2  2656  gencbval  2729  vtoclgaf  2746  vtocl2gaf  2748  vtocl3gaf  2750  rspct  2777  rspc  2778  rspc2gv  2796  ceqex  2807  ralab2  2843  mob2  2859  mob  2861  morex  2863  reu7  2874  reu8  2875  nelrdva  2886  cdeqim  2897  sbcimg  2945  csbhypf  3033  cbvralcsf  3057  dfss2f  3083  sbcssg  3467  sneqrg  3684  elintab  3777  intss1  3781  intmin  3786  dfiin2g  3841  disji2  3917  disjiun  3919  trel  4028  trss  4030  bnd2  4092  zfpow  4094  exmidexmid  4115  exmidsssnc  4121  exmidundifim  4125  rext  4132  opth  4154  copsexg  4161  poeq1  4216  pocl  4220  swopolem  4222  swopo  4223  soeq1  4232  sowlin  4237  frforeq2  4262  frforeq3  4264  frirrg  4267  frind  4269  weeq1  4273  ordelord  4298  reusv3i  4375  ordtriexmid  4432  ontr2exmid  4435  onsucsssucexmid  4437  onsucelsucexmid  4440  ordsucunielexmid  4441  regexmidlem1  4443  regexmid  4445  reg2exmid  4446  elirr  4451  en2lp  4464  ordsoexmid  4472  onintexmid  4482  reg3exmid  4489  tfis  4492  tfisi  4496  peano2  4504  findes  4512  nnregexmid  4529  omsinds  4530  vtoclr  4582  poinxp  4603  soinxp  4604  posng  4606  ssrel  4622  ssrel2  4624  ssrelrel  4634  relop  4684  issref  4916  iota5  5103  dffun4f  5134  sbcfung  5142  funopg  5152  brprcneu  5407  funfveu  5427  tz6.12f  5443  funbrfv  5453  ssimaexg  5476  fvmptss2  5489  fvmptssdm  5498  fvmptf  5506  fvelrn  5544  f1veqaeq  5663  dff13f  5664  isopolem  5716  isosolem  5718  riota5f  5747  imbrov2fvoveq  5792  oprabid  5796  ovmpos  5887  ov2gf  5888  ovi3  5900  caovcan  5928  caovordig  5929  caofrss  5999  caoftrn  6000  dfoprab4f  6084  f1o2ndf1  6118  poxp  6122  smoel  6190  tfrlem1  6198  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  nnsucelsuc  6380  nnsucsssuc  6381  nnmordi  6405  nnaordex  6416  qsel  6499  eroveu  6513  ecopovtrn  6519  ecopovtrng  6522  th3qlem2  6525  ixpsnf1o  6623  fundmeng  6694  phplem3g  6743  nneneq  6744  ssfiexmid  6763  domfiexmid  6765  findcard  6775  findcard2  6776  findcard2s  6777  findcard2d  6778  findcard2sd  6779  diffifi  6781  ac6sfi  6785  fiintim  6810  fisseneq  6813  fidcenumlemrk  6835  fidcenumlemr  6836  isbth  6848  supeq3  6870  supeq123d  6871  supmoti  6873  suplubti  6880  supisolem  6888  cnvinfex  6898  eqinfti  6900  infvalti  6902  ordiso2  6913  isomni  7001  finomni  7005  exmidomni  7007  ctssexmid  7017  ismkv  7020  ismkvnex  7022  mkvprop  7025  fodjumkvlemres  7026  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  ccfunen  7072  ltsonq  7199  ltexnqq  7209  prcdnql  7285  prcunqu  7286  prloc  7292  prdisj  7293  genprndl  7322  genprndu  7323  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemcl  7477  caucvgprprlemcbv  7488  caucvgprprlemval  7489  suplocexprlemloc  7522  lttrsr  7563  ltsosr  7565  recexgt0sr  7574  mulgt0sr  7579  aptisr  7580  mulextsr1  7582  srpospr  7584  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  caucvgsr  7603  map2psrprg  7606  suplocsrlemb  7607  axprecex  7681  axpre-ltwlin  7684  axpre-lttrn  7685  axpre-apti  7686  axpre-mulgt0  7688  axpre-mulext  7689  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  axsuploc  7830  ltleletr  7839  ltordlem  8237  squeeze0  8655  sup3exmid  8708  nnsub  8752  fzind  9159  uzind4s  9378  uzind4s2  9379  indstr  9381  supinfneg  9383  infsupneg  9384  frec2uzuzd  10168  frec2uzltd  10169  uzsinds  10208  seq3fveq2  10235  seq3shft2  10239  monoord  10242  seq3split  10245  seq3id2  10275  expcl2lemap  10298  facdiv  10477  facwordi  10479  zfz1isolem1  10576  zfz1iso  10577  seq3coll  10578  caucvgre  10746  fimaxre2  10991  climcn1  11070  climcn2  11071  subcn2  11073  summodclem2a  11143  fsumsplitf  11170  fsum2d  11197  modfsummod  11220  fsumabs  11227  telfsumo  11228  fsumiun  11239  prodfdivap  11309  ndvdssub  11616  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemzz  11679  bezoutlemsup  11686  dfgcd2  11691  algcvg  11718  algcvga  11721  algfx  11722  lcmgcdlem  11747  lcmdvds  11749  coprmgcdb  11758  coprmdvds1  11761  coprmdvds2  11763  prmind2  11790  dvdsprime  11792  nprm  11793  dvdsprm  11806  exprmfct  11807  coprm  11811  isprm6  11814  prmfac1  11819  sqrt2irr  11829  ennnfonelemim  11926  exmidunben  11928  uniopn  12157  fiinopn  12160  epttop  12248  cnpval  12356  iscnp  12357  icnpimaex  12369  lmcvg  12375  cnptoprest  12397  cnptoprest2  12398  lmss  12404  lmff  12407  txcnp  12429  txlm  12437  cnmpt12  12445  cnmpt22  12452  blssps  12585  blss  12586  metss  12652  comet  12657  metcnp3  12669  metcnp2  12671  txmetcnp  12676  divcnap  12713  elcncf2  12719  cncfi  12723  mulc1cncf  12734  cncfmet  12737  mulcncflem  12748  mulcncf  12749  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeulemeu  12758  suplociccreex  12760  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemeu  12767  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemloc  12777  limccl  12786  ellimc3apf  12787  limccnpcntop  12802  limccnp2lem  12803  limccoap  12805  dvcoapbr  12829  cbvrald  12984  bj-bdfindes  13136  bj-omtrans  13143  bj-inf2vnlem1  13157  bj-inf2vnlem2  13158  bj-inf2vnlem3  13159  bj-inf2vnlem4  13160  bj-findes  13168  strcoll2  13170  sscoll2  13175  exmid1stab  13184  subctctexmid  13185  exmidsbthrlem  13206  sbthom  13210
  Copyright terms: Public domain W3C validator