Theorem imbi12d 233

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	|- ( ph -> ( ps <-> ch ) )
imbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
imbi12d	|- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	imbi1d 230	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 229	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

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  822  nfbidf  1527  drnf1  1721  drnf2  1722  equveli  1747  ax11v2  1808  ax11v  1815  ax11ev  1816  equs5or  1818  mobidh  2048  mobid  2049  axext3  2148  cbvralfw  2683  cbvralf  2685  cbvralvw  2696  cbvraldva2  2699  gencbval  2774  vtoclgaf  2791  vtocl2gaf  2793  vtocl3gaf  2795  rspct  2823  rspc  2824  rspc2gv  2842  ceqex  2853  ralab2  2890  mob2  2906  mob  2908  morex  2910  reu7  2921  reu8  2922  nelrdva  2933  cdeqim  2944  sbcimg  2992  csbhypf  3083  cbvralcsf  3107  dfss2f  3133  sbcssg  3518  sneqrg  3742  elintab  3835  intss1  3839  intmin  3844  dfiin2g  3899  disji2  3975  disjiun  3977  trel  4087  trss  4089  bnd2  4152  zfpow  4154  exmidexmid  4175  exmidsssnc  4182  exmidundifim  4186  rext  4193  opth  4215  copsexg  4222  poeq1  4277  pocl  4281  swopolem  4283  swopo  4284  soeq1  4293  sowlin  4298  frforeq2  4323  frforeq3  4325  frirrg  4328  frind  4330  weeq1  4334  ordelord  4359  reusv3i  4437  ordtriexmid  4498  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  ordsucunielexmid  4508  regexmidlem1  4510  regexmid  4512  reg2exmid  4513  elirr  4518  en2lp  4531  ordsoexmid  4539  onintexmid  4550  reg3exmid  4557  tfis  4560  tfisi  4564  peano2  4572  findes  4580  nnregexmid  4598  omsinds  4599  vtoclr  4652  poinxp  4673  soinxp  4674  posng  4676  ssrel  4692  ssrel2  4694  ssrelrel  4704  relop  4754  issref  4986  iota5  5173  dffun4f  5204  sbcfung  5212  funopg  5222  brprcneu  5479  funfveu  5499  tz6.12f  5515  funbrfv  5525  ssimaexg  5548  fvmptss2  5561  fvmptssdm  5570  fvmptf  5578  fvelrn  5616  f1veqaeq  5737  dff13f  5738  isopolem  5790  isosolem  5792  riota5f  5822  imbrov2fvoveq  5867  oprabid  5874  ovmpos  5965  ov2gf  5966  ovi3  5978  caovcan  6006  caovordig  6007  caofrss  6074  caoftrn  6075  dfoprab4f  6161  f1o2ndf1  6196  poxp  6200  smoel  6268  tfrlem1  6276  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemaccex  6329  tfrcllemres  6330  tfrcl  6332  nnsucelsuc  6459  nnsucsssuc  6460  nnmordi  6484  nnaordex  6495  qsel  6578  eroveu  6592  ecopovtrn  6598  ecopovtrng  6601  th3qlem2  6604  ixpsnf1o  6702  fundmeng  6773  phplem3g  6822  nneneq  6823  ssfiexmid  6842  domfiexmid  6844  findcard  6854  findcard2  6855  findcard2s  6856  findcard2d  6857  findcard2sd  6858  diffifi  6860  ac6sfi  6864  fiintim  6894  fisseneq  6897  fidcenumlemrk  6919  fidcenumlemr  6920  isbth  6932  supeq3  6955  supeq123d  6956  supmoti  6958  suplubti  6965  supisolem  6973  cnvinfex  6983  eqinfti  6985  infvalti  6987  ordiso2  7000  nnnninfeq2  7093  isomni  7100  finomni  7104  exmidomni  7106  ctssexmid  7114  ismkv  7117  ismkvnex  7119  mkvprop  7122  fodjumkvlemres  7123  enmkvlem  7125  iswomni  7129  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  ccfunen  7205  ltsonq  7339  ltexnqq  7349  prcdnql  7425  prcunqu  7426  prloc  7432  prdisj  7433  genprndl  7462  genprndu  7463  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemcl  7617  caucvgprprlemcbv  7628  caucvgprprlemval  7629  suplocexprlemloc  7662  lttrsr  7703  ltsosr  7705  recexgt0sr  7714  mulgt0sr  7719  aptisr  7720  mulextsr1  7722  srpospr  7724  caucvgsrlemgt1  7736  caucvgsrlemoffres  7741  caucvgsr  7743  map2psrprg  7746  suplocsrlemb  7747  axprecex  7821  axpre-ltwlin  7824  axpre-lttrn  7825  axpre-apti  7826  axpre-mulgt0  7828  axpre-mulext  7829  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  axsuploc  7971  ltleletr  7980  ltordlem  8380  squeeze0  8799  sup3exmid  8852  nnsub  8896  fzind  9306  uzind4s  9528  uzind4s2  9529  indstr  9531  supinfneg  9533  infsupneg  9534  frec2uzuzd  10337  frec2uzltd  10338  uzsinds  10377  seq3fveq2  10404  seq3shft2  10408  monoord  10411  seq3split  10414  seq3id2  10444  expcl2lemap  10467  nn0ltexp2  10623  facdiv  10651  facwordi  10653  zfz1isolem1  10753  zfz1iso  10754  seq3coll  10755  caucvgre  10923  fimaxre2  11168  climcn1  11249  climcn2  11250  subcn2  11252  summodclem2a  11322  fsumsplitf  11349  fsum2d  11376  modfsummod  11399  fsumabs  11406  telfsumo  11407  fsumiun  11418  prodfdivap  11488  fprod2d  11564  fproddivapf  11572  fprodsplitf  11573  fprodsplit1f  11575  ndvdssub  11867  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemzz  11935  bezoutlemsup  11942  dfgcd2  11947  algcvg  11980  algcvga  11983  algfx  11984  lcmgcdlem  12009  lcmdvds  12011  coprmgcdb  12020  coprmdvds1  12023  coprmdvds2  12025  prmind2  12052  dvdsprime  12054  nprm  12055  dvdsprm  12069  exprmfct  12070  isprm5lem  12073  coprm  12076  isprm6  12079  prmfac1  12084  sqrt2irr  12094  pcqmul  12235  pcqcl  12238  pc2dvds  12261  pcz  12263  prmpwdvds  12285  ennnfonelemim  12357  exmidunben  12359  infpn2  12389  uniopn  12639  fiinopn  12642  epttop  12730  cnpval  12838  iscnp  12839  icnpimaex  12851  lmcvg  12857  cnptoprest  12879  cnptoprest2  12880  lmss  12886  lmff  12889  txcnp  12911  txlm  12919  cnmpt12  12927  cnmpt22  12934  blssps  13067  blss  13068  metss  13134  comet  13139  metcnp3  13151  metcnp2  13153  txmetcnp  13158  divcnap  13195  elcncf2  13201  cncfi  13205  mulc1cncf  13216  cncfmet  13219  mulcncflem  13230  mulcncf  13231  dedekindeulemloc  13237  dedekindeulemlu  13239  dedekindeulemeu  13240  suplociccreex  13242  dedekindicclemloc  13246  dedekindicclemlu  13248  dedekindicclemeu  13249  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  limccl  13268  ellimc3apf  13269  limccnpcntop  13284  limccnp2lem  13285  limccoap  13287  dvcoapbr  13311  lgsdir2lem4  13572  2sqlem6  13596  2sqlem8  13599  2sqlem10  13601  cbvrald  13669  bj-bdfindes  13831  bj-omtrans  13838  bj-inf2vnlem1  13852  bj-inf2vnlem2  13853  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  bj-findes  13863  strcoll2  13865  sscoll2  13870  exmid1stab  13880  subctctexmid  13881  pw1nct  13883  exmidsbthrlem  13901  sbthom  13905  apdiff  13927  ismkvnnlem  13931  nconstwlpolem  13943  neapmkv  13946