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:  stbid  775  nfbidf  1475  drnf1  1665  drnf2  1666  equveli  1686  ax11v2  1745  ax11v  1752  ax11ev  1753  equs5or  1755  mobidh  1979  mobid  1980  axext3  2068  cbvralf  2580  cbvraldva2  2590  gencbval  2661  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  rspct  2708  rspc  2709  rspc2gv  2725  ceqex  2735  ralab2  2770  mob2  2786  mob  2788  morex  2790  reu7  2801  reu8  2802  nelrdva  2811  cdeqim  2822  sbcimg  2869  csbhypf  2955  cbvralcsf  2979  dfss2f  3005  sbcssg  3378  sneqrg  3591  elintab  3684  intss1  3688  intmin  3693  dfiin2g  3748  trel  3920  trss  3922  bnd2  3985  zfpow  3987  exmidexmid  4007  rext  4018  opth  4040  copsexg  4047  poeq1  4102  pocl  4106  swopolem  4108  swopo  4109  soeq1  4118  sowlin  4123  frforeq2  4148  frforeq3  4150  frirrg  4153  frind  4155  weeq1  4159  ordelord  4184  reusv3i  4257  ordtriexmid  4313  ontr2exmid  4316  onsucsssucexmid  4318  onsucelsucexmid  4321  ordsucunielexmid  4322  regexmidlem1  4324  regexmid  4326  reg2exmid  4327  elirr  4332  en2lp  4345  ordsoexmid  4353  onintexmid  4363  reg3exmid  4370  tfis  4373  tfisi  4377  peano2  4385  findes  4393  nnregexmid  4409  omsinds  4410  vtoclr  4456  poinxp  4477  soinxp  4478  posng  4480  ssrel  4496  ssrel2  4498  ssrelrel  4508  relop  4556  issref  4783  iota5  4968  dffun4f  4999  sbcfung  5006  funopg  5015  brprcneu  5263  funfveu  5283  tz6.12f  5298  funbrfv  5308  ssimaexg  5331  fvmptss2  5344  fvmptssdm  5352  fvmptf  5360  fvelrn  5395  f1veqaeq  5511  dff13f  5512  isopolem  5564  isosolem  5566  riota5f  5595  oprabid  5640  ovmpt2s  5727  ov2gf  5728  ovi3  5740  caovcan  5768  caovordig  5769  caofrss  5838  caoftrn  5839  dfoprab4f  5922  f1o2ndf1  5952  poxp  5956  smoel  6021  tfrlem1  6029  tfr1onlemsucfn  6061  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemaccex  6069  tfr1onlemres  6070  tfrcllemsucfn  6074  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemaccex  6082  tfrcllemres  6083  tfrcl  6085  nnsucelsuc  6208  nnsucsssuc  6209  nnmordi  6229  nnaordex  6240  qsel  6323  eroveu  6337  ecopovtrn  6343  ecopovtrng  6346  th3qlem2  6349  fundmeng  6478  phplem3g  6526  nneneq  6527  ssfiexmid  6546  domfiexmid  6548  findcard  6558  findcard2  6559  findcard2s  6560  findcard2d  6561  findcard2sd  6562  diffifi  6564  ac6sfi  6568  fisseneq  6595  isbth  6623  supeq3  6632  supeq123d  6633  supmoti  6635  suplubti  6642  supisolem  6650  cnvinfex  6660  eqinfti  6662  infvalti  6664  ordiso2  6675  isomni  6739  finomni  6743  exmidomni  6745  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  ltsonq  6904  ltexnqq  6914  prcdnql  6990  prcunqu  6991  prloc  6997  prdisj  6998  genprndl  7027  genprndu  7028  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemcl  7182  caucvgprprlemcbv  7193  caucvgprprlemval  7194  lttrsr  7255  ltsosr  7257  recexgt0sr  7266  mulgt0sr  7270  aptisr  7271  mulextsr1  7273  srpospr  7275  caucvgsrlemgt1  7287  caucvgsrlemoffres  7292  caucvgsr  7294  axprecex  7362  axpre-ltwlin  7365  axpre-lttrn  7366  axpre-apti  7367  axpre-mulgt0  7369  axpre-mulext  7370  axcaucvglemcau  7380  axcaucvglemres  7381  ltleletr  7514  squeeze0  8303  nnsub  8398  fzind  8797  uzind4s  9013  uzind4s2  9014  indstr  9016  supinfneg  9018  infsupneg  9019  frec2uzuzd  9740  frec2uzltd  9741  uzsinds  9779  iseqfveq2  9820  iseqshft2  9824  monoord  9829  iseqsplit  9832  iseqid2  9863  expcl2lemap  9887  facdiv  10064  facwordi  10066  zfz1isolem1  10163  zfz1iso  10164  iseqcoll  10165  caucvgre  10331  fimaxre2  10574  climcn1  10613  climcn2  10614  subcn2  10616  isummolem2a  10684  fsumsplitf  10709  ndvdssub  10855  bezoutlemmain  10912  bezoutlemex  10915  bezoutlemzz  10916  bezoutlemsup  10923  dfgcd2  10928  ialgcvg  10955  ialgcvga  10958  ialgfx  10959  lcmgcdlem  10984  lcmdvds  10986  coprmgcdb  10995  coprmdvds1  10998  coprmdvds2  11000  prmind2  11027  dvdsprime  11029  nprm  11030  dvdsprm  11043  exprmfct  11044  coprm  11048  isprm6  11051  prmfac1  11056  sqrt2irr  11066  cbvrald  11176  bj-bdfindes  11332  bj-omtrans  11339  bj-inf2vnlem1  11353  bj-inf2vnlem2  11354  bj-inf2vnlem3  11355  bj-inf2vnlem4  11356  bj-findes  11364  strcoll2  11366  sscoll2  11371  exmidsbthrlem  11400
  Copyright terms: Public domain W3C validator