Theorem imbi12d 234

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 231	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 230	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  stbid  844  nfbidf  1592  drnf1  1786  drnf2  1787  equveli  1812  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  mobidh  2120  mobid  2121  axext3  2221  cbvralfw  2775  cbvralf  2777  cbvralvw  2790  cbvraldva2  2793  gencbval  2871  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspc2gv  2942  ceqex  2953  ralab2  2990  mob2  3006  mob  3008  morex  3010  reu7  3021  reu8  3022  nelrdva  3033  cdeqim  3044  sbcimg  3093  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  sbcssg  3636  ifeqeqxdc  3687  sneqrg  3887  elintab  3981  intss1  3985  intmin  3990  dfiin2g  4045  disji2  4122  disjiun  4125  trel  4236  trss  4238  bnd2  4310  zfpow  4312  exmidexmid  4333  exmidsssnc  4340  exmidundifim  4344  exmid1stab  4345  rext  4355  opth  4377  copsexg  4384  poeq1  4444  pocl  4448  swopolem  4450  swopo  4451  soeq1  4460  sowlin  4465  frforeq2  4490  frforeq3  4492  frirrg  4495  frind  4497  weeq1  4501  ordelord  4526  reusv3i  4605  ordtriexmid  4668  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  regexmid  4682  reg2exmid  4683  elirr  4688  en2lp  4701  ordsoexmid  4709  onintexmid  4720  reg3exmid  4727  tfis  4730  tfisi  4734  peano2  4742  findes  4750  nnregexmid  4768  omsinds  4769  vtoclr  4823  poinxp  4844  soinxp  4845  posng  4847  ssrel  4863  ssrel2  4865  ssrelrel  4875  relop  4930  issref  5170  iotaexab  5356  iota5  5359  dffun4f  5393  sbcfung  5401  funopg  5411  brprcneu  5688  funfveu  5708  tz6.12f  5724  funbrfv  5739  ssimaexg  5765  fvmptss2  5780  fvmptssdm  5790  fvmptf  5798  fvelrn  5839  f1veqaeq  5975  dff13f  5976  isopolem  6028  isosolem  6030  riota5f  6065  imbrov2fvoveq  6110  oprabid  6117  ovmpos  6212  ov2gf  6213  ovi3  6226  caovcan  6254  caovordig  6255  caofrss  6334  caoftrn  6335  dfoprab4f  6427  f1o2ndf1  6464  poxp  6468  suppfnss  6497  smoel  6571  tfrlem1  6579  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemaccex  6632  tfrcllemres  6633  tfrcl  6635  nnsucelsuc  6764  nnsucsssuc  6765  nnmordi  6789  nnaordex  6801  qsel  6886  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  ixpsnf1o  7018  fundmeng  7095  modom  7108  phplem3g  7157  nneneq  7158  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  supeq3  7330  supeq123d  7331  supmoti  7333  suplubti  7340  supisolem  7348  cnvinfex  7358  eqinfti  7360  infvalti  7362  ordiso2  7375  nninfninc  7463  nnnninfeq2  7469  isomni  7476  finomni  7480  exmidomni  7482  ctssexmid  7490  ismkv  7493  ismkvnex  7495  mkvprop  7498  fodjumkvlemres  7499  enmkvlem  7501  iswomni  7505  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papeq1  7609  papsym  7612  papcotr  7613  tapeq1  7618  exmidapne  7626  ccfunen  7630  ltsonq  7765  ltexnqq  7775  prcdnql  7851  prcunqu  7852  prloc  7858  prdisj  7859  genprndl  7888  genprndu  7889  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemcl  8043  caucvgprprlemcbv  8054  caucvgprprlemval  8055  suplocexprlemloc  8088  lttrsr  8129  ltsosr  8131  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  suplocsrlemb  8173  axprecex  8247  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  axsuploc  8398  ltleletr  8407  ltordlem  8811  squeeze0  9236  sup3exmid  9289  nnsub  9345  fzind  9765  uzind4s  9999  uzind4s2  10000  indstr  10002  supinfneg  10004  infsupneg  10005  frec2uzuzd  10852  frec2uzltd  10853  uzsinds  10894  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  seqf1oglem2  10970  seqf1og  10971  seq3id2  10976  seqhomog  10980  expcl2lemap  11001  nn0ltexp2  11161  facdiv  11190  facwordi  11192  zfz1isolem1  11306  zfz1iso  11307  seq3coll  11308  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccat3blem  11525  reuccatpfxs1lem  11532  caucvgre  11761  fimaxre2  12008  climcn1  12090  climcn2  12091  subcn2  12093  summodclem2a  12164  fsumsplitf  12191  fsum2d  12218  modfsummod  12241  fsumabs  12248  telfsumo  12249  fsumiun  12260  prodfdivap  12330  fprod2d  12406  fproddivapf  12414  fprodsplitf  12415  fprodsplit1f  12417  ndvdssub  12713  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemzz  12795  bezoutlemsup  12802  dfgcd2  12807  algcvg  12842  algcvga  12845  algfx  12846  lcmgcdlem  12871  lcmdvds  12873  coprmgcdb  12882  coprmdvds1  12885  coprmdvds2  12887  prmind2  12914  dvdsprime  12916  nprm  12917  dvdsprm  12932  exprmfct  12933  isprm5lem  12936  coprm  12939  isprm6  12942  prmfac1  12947  sqrt2irr  12957  pcqmul  13102  pcqcl  13105  pc2dvds  13129  pcz  13131  prmpwdvds  13154  prmlem0  13240  ballotfilem2  13277  ennnfonelemim  13364  exmidunben  13366  infpn2  13396  setscomd  13442  mhmlem  13966  isnsg2  14055  ghmf1  14125  islring  14548  lringuplu  14552  opprlring  14553  rrgval  14619  rrgeq0i  14621  isdomn  14627  domneq0  14630  opprdomnbg  14632  znidom  15041  znrrg  15044  mplvalcoe  15130  mplsubgfilemcl  15139  uniopn  15151  fiinopn  15154  epttop  15240  cnpval  15348  iscnp  15349  icnpimaex  15361  lmcvg  15367  cnptoprest  15389  cnptoprest2  15390  lmss  15396  lmff  15399  txcnp  15421  txlm  15429  cnmpt12  15437  cnmpt22  15444  blssps  15577  blss  15578  metss  15644  comet  15649  metcnp3  15661  metcnp2  15663  txmetcnp  15668  divcnap  15715  mpomulcn  15716  elcncf2  15724  cncfi  15728  mulc1cncf  15739  cncfmet  15742  mulcncflem  15757  mulcncf  15758  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeulemeu  15772  suplociccreex  15774  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemeu  15781  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthreinc  15795  limccl  15809  ellimc3apf  15810  limccnpcntop  15825  limccnp2lem  15826  limccoap  15828  dvcoapbr  15857  dvmptfsum  15875  mpodvdsmulf1o  16185  perfectlem2  16198  bcmono  16202  lgsdir2lem4  16248  gausslemma2dlem0i  16274  lgseisenlem2  16288  lgsquad2lem2  16299  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  gropd  16386  grstructd2dom  16387  upgredg2vtx  16487  upgredgpr  16488  eupth2fi  16818  lealltlt1  16849  lealltlt2  16850  dichmul0orlem7  16857  cbvrald  16914  bj-bdfindes  17073  bj-omtrans  17080  bj-inf2vnlem1  17094  bj-inf2vnlem2  17095  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  bj-findes  17105  strcoll2  17107  sscoll2  17112  subctctexmid  17128  pw1nct  17131  exmidnotnotr  17134  exmidcon  17135  wexmiddiffilem  17141  wexmiddifxy  17144  exmidsbthrlem  17165  sbthom  17169  apdiff  17195  ismkvnnlem  17200  nconstwlpolem  17213  neapmkv  17216  neap0mkv  17217  ltlenmkv  17218  alsbid  17241  cbvals  17244