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 ) ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced 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  3633  ifeqeqxdc  3684  sneqrg  3882  elintab  3976  intss1  3980  intmin  3985  dfiin2g  4040  disji2  4117  disjiun  4120  trel  4231  trss  4233  bnd2  4305  zfpow  4307  exmidexmid  4328  exmidsssnc  4335  exmidundifim  4339  exmid1stab  4340  rext  4350  opth  4372  copsexg  4379  poeq1  4439  pocl  4443  swopolem  4445  swopo  4446  soeq1  4455  sowlin  4460  frforeq2  4485  frforeq3  4487  frirrg  4490  frind  4492  weeq1  4496  ordelord  4521  reusv3i  4600  ordtriexmid  4663  ontr2exmid  4667  onsucsssucexmid  4669  onsucelsucexmid  4672  ordsucunielexmid  4673  regexmidlem1  4675  regexmid  4677  reg2exmid  4678  elirr  4683  en2lp  4696  ordsoexmid  4704  onintexmid  4715  reg3exmid  4722  tfis  4725  tfisi  4729  peano2  4737  findes  4745  nnregexmid  4763  omsinds  4764  vtoclr  4818  poinxp  4839  soinxp  4840  posng  4842  ssrel  4858  ssrel2  4860  ssrelrel  4870  relop  4925  issref  5165  iotaexab  5351  iota5  5354  dffun4f  5388  sbcfung  5396  funopg  5406  brprcneu  5683  funfveu  5703  tz6.12f  5719  funbrfv  5733  ssimaexg  5759  fvmptss2  5774  fvmptssdm  5784  fvmptf  5792  fvelrn  5830  f1veqaeq  5965  dff13f  5966  isopolem  6018  isosolem  6020  riota5f  6055  imbrov2fvoveq  6100  oprabid  6107  ovmpos  6202  ov2gf  6203  ovi3  6216  caovcan  6244  caovordig  6245  caofrss  6324  caoftrn  6325  dfoprab4f  6417  f1o2ndf1  6454  poxp  6458  suppfnss  6487  smoel  6561  tfrlem1  6569  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemaccex  6622  tfrcllemres  6623  tfrcl  6625  nnsucelsuc  6754  nnsucsssuc  6755  nnmordi  6779  nnaordex  6791  qsel  6876  eroveu  6890  ecopovtrn  6896  ecopovtrng  6899  th3qlem2  6902  ixpsnf1o  7008  fundmeng  7085  modom  7098  phplem3g  7147  nneneq  7148  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  findcard  7182  findcard2  7183  findcard2s  7184  findcard2d  7185  findcard2sd  7186  diffifi  7188  ac6sfi  7192  fiintim  7228  fisseneq  7232  fidcenumlemrk  7261  fidcenumlemr  7262  isbth  7274  supeq3  7320  supeq123d  7321  supmoti  7323  suplubti  7330  supisolem  7338  cnvinfex  7348  eqinfti  7350  infvalti  7352  ordiso2  7365  nninfninc  7453  nnnninfeq2  7459  isomni  7466  finomni  7470  exmidomni  7472  ctssexmid  7480  ismkv  7483  ismkvnex  7485  mkvprop  7488  fodjumkvlemres  7489  enmkvlem  7491  iswomni  7495  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  papeq1  7599  papsym  7602  papcotr  7603  tapeq1  7608  exmidapne  7616  ccfunen  7620  ltsonq  7755  ltexnqq  7765  prcdnql  7841  prcunqu  7842  prloc  7848  prdisj  7849  genprndl  7878  genprndu  7879  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemcl  8033  caucvgprprlemcbv  8044  caucvgprprlemval  8045  suplocexprlemloc  8078  lttrsr  8119  ltsosr  8121  recexgt0sr  8130  mulgt0sr  8135  aptisr  8136  mulextsr1  8138  srpospr  8140  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  caucvgsr  8159  map2psrprg  8162  suplocsrlemb  8163  axprecex  8237  axpre-ltwlin  8240  axpre-lttrn  8241  axpre-apti  8242  axpre-mulgt0  8244  axpre-mulext  8245  axcaucvglemcau  8255  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  axsuploc  8388  ltleletr  8397  ltordlem  8800  squeeze0  9224  sup3exmid  9277  nnsub  9322  fzind  9740  uzind4s  9969  uzind4s2  9970  indstr  9972  supinfneg  9974  infsupneg  9975  frec2uzuzd  10817  frec2uzltd  10818  uzsinds  10859  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  seqf1oglem2  10935  seqf1og  10936  seq3id2  10941  seqhomog  10945  expcl2lemap  10966  nn0ltexp2  11125  facdiv  11154  facwordi  11156  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  swrdccat3blem  11489  reuccatpfxs1lem  11496  caucvgre  11725  fimaxre2  11971  climcn1  12052  climcn2  12053  subcn2  12055  summodclem2a  12126  fsumsplitf  12153  fsum2d  12180  modfsummod  12203  fsumabs  12210  telfsumo  12211  fsumiun  12222  prodfdivap  12292  fprod2d  12368  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  ndvdssub  12675  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemzz  12757  bezoutlemsup  12764  dfgcd2  12769  algcvg  12804  algcvga  12807  algfx  12808  lcmgcdlem  12833  lcmdvds  12835  coprmgcdb  12844  coprmdvds1  12847  coprmdvds2  12849  prmind2  12876  dvdsprime  12878  nprm  12879  dvdsprm  12893  exprmfct  12894  isprm5lem  12897  coprm  12900  isprm6  12903  prmfac1  12908  sqrt2irr  12918  pcqmul  13060  pcqcl  13063  pc2dvds  13087  pcz  13089  prmpwdvds  13112  ballotfilem2  13206  ennnfonelemim  13293  exmidunben  13295  infpn2  13325  setscomd  13371  mhmlem  13894  isnsg2  13983  ghmf1  14053  islring  14472  lringuplu  14476  opprlring  14477  rrgval  14543  rrgeq0i  14545  isdomn  14551  domneq0  14554  opprdomnbg  14556  znidom  14964  znrrg  14967  mplvalcoe  15004  mplsubgfilemcl  15013  uniopn  15025  fiinopn  15028  epttop  15114  cnpval  15222  iscnp  15223  icnpimaex  15235  lmcvg  15241  cnptoprest  15263  cnptoprest2  15264  lmss  15270  lmff  15273  txcnp  15295  txlm  15303  cnmpt12  15311  cnmpt22  15318  blssps  15451  blss  15452  metss  15518  comet  15523  metcnp3  15535  metcnp2  15537  txmetcnp  15542  divcnap  15589  mpomulcn  15590  elcncf2  15598  cncfi  15602  mulc1cncf  15613  cncfmet  15616  mulcncflem  15631  mulcncf  15632  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeulemeu  15646  suplociccreex  15648  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicclemeu  15655  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthreinc  15669  limccl  15683  ellimc3apf  15684  limccnpcntop  15699  limccnp2lem  15700  limccoap  15702  dvcoapbr  15731  dvmptfsum  15749  mpodvdsmulf1o  16018  perfectlem2  16028  lgsdir2lem4  16064  gausslemma2dlem0i  16090  lgseisenlem2  16104  lgsquad2lem2  16115  2sqlem6  16153  2sqlem8  16156  2sqlem10  16158  gropd  16202  grstructd2dom  16203  upgredg2vtx  16303  upgredgpr  16304  eupth2fi  16634  lealltlt1  16665  lealltlt2  16666  dichmul0orlem7  16673  cbvrald  16730  bj-bdfindes  16889  bj-omtrans  16896  bj-inf2vnlem1  16910  bj-inf2vnlem2  16911  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  bj-findes  16921  strcoll2  16923  sscoll2  16928  subctctexmid  16944  pw1nct  16947  exmidnotnotr  16949  exmidcon  16950  exmidsbthrlem  16972  sbthom  16976  apdiff  17002  ismkvnnlem  17007  nconstwlpolem  17020  neapmkv  17023  neap0mkv  17024  ltlenmkv  17025