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

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi1d 229	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 228	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 186	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

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:  nfbidf  1472  drnf1  1661  drnf2  1662  equveli  1682  ax11v2  1741  ax11v  1748  ax11ev  1749  equs5or  1751  mobidh  1975  mobid  1976  axext3  2064  cbvralf  2571  cbvraldva2  2581  gencbval  2647  vtoclgaf  2663  vtocl2gaf  2665  vtocl3gaf  2667  rspct  2694  rspc  2695  rspc2gv  2712  ceqex  2722  ralab2  2756  mob2  2772  mob  2774  morex  2776  reu7  2787  reu8  2788  nelrdva  2797  cdeqim  2808  sbcimg  2855  csbhypf  2941  cbvralcsf  2964  dfss2f  2990  sbcssg  3350  sneqrg  3554  elintab  3647  intss1  3651  intmin  3656  dfiin2g  3711  trel  3882  trss  3884  bnd2  3947  zfpow  3949  rext  3970  opth  3992  copsexg  3999  poeq1  4054  pocl  4058  swopolem  4060  swopo  4061  soeq1  4070  sowlin  4075  frforeq2  4100  frforeq3  4102  frirrg  4105  frind  4107  weeq1  4111  ordelord  4136  reusv3i  4209  ordtriexmid  4265  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  ordsucunielexmid  4274  regexmidlem1  4276  regexmid  4278  reg2exmid  4279  elirr  4284  en2lp  4297  ordsoexmid  4305  onintexmid  4315  reg3exmid  4322  tfis  4324  tfisi  4328  peano2  4336  findes  4344  nnregexmid  4360  vtoclr  4406  poinxp  4427  soinxp  4428  posng  4430  ssrel  4446  ssrel2  4448  ssrelrel  4458  relop  4504  issref  4727  iota5  4907  dffun4f  4938  sbcfung  4945  funopg  4954  brprcneu  5191  funfveu  5208  tz6.12f  5223  funbrfv  5233  ssimaexg  5256  fvmptss2  5268  fvmptssdm  5276  fvmptf  5284  fvelrn  5319  f1veqaeq  5429  dff13f  5430  isopolem  5481  isosolem  5483  riota5f  5512  oprabid  5557  ovmpt2s  5644  ov2gf  5645  ovi3  5657  caovcan  5685  caovordig  5686  caofrss  5755  caoftrn  5756  dfoprab4f  5839  f1o2ndf1  5869  poxp  5873  smoel  5938  tfrlem1  5946  nnsucelsuc  6093  nnsucsssuc  6094  nnmordi  6112  nnaordex  6123  qsel  6206  eroveu  6220  ecopovtrn  6226  ecopovtrng  6229  th3qlem2  6232  fundmeng  6310  phplem3g  6342  nneneq  6343  ssfiexmid  6361  domfiexmid  6363  findcard  6372  findcard2  6373  findcard2s  6374  findcard2d  6375  findcard2sd  6376  diffifi  6378  ac6sfi  6379  supeq3  6403  supeq123d  6404  supmoti  6406  suplubti  6413  supisolem  6421  cnvinfex  6431  eqinfti  6433  infvalti  6435  ordiso2  6446  ltsonq  6588  ltexnqq  6598  prcdnql  6674  prcunqu  6675  prloc  6681  prdisj  6682  genprndl  6711  genprndu  6712  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemcl  6866  caucvgprprlemcbv  6877  caucvgprprlemval  6878  lttrsr  6939  ltsosr  6941  recexgt0sr  6950  mulgt0sr  6954  aptisr  6955  mulextsr1  6957  srpospr  6959  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  axprecex  7046  axpre-ltwlin  7049  axpre-lttrn  7050  axpre-apti  7051  axpre-mulgt0  7053  axpre-mulext  7054  axcaucvglemcau  7064  axcaucvglemres  7065  ltleletr  7193  squeeze0  7982  nnsub  8077  fzind  8462  uzind4s  8678  uzind4s2  8679  indstr  8681  supinfneg  8683  infsupneg  8684  frec2uzzd  9402  frec2uzuzd  9404  frec2uzltd  9405  uzsinds  9428  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  expcl2lemap  9488  facdiv  9665  facwordi  9667  caucvgre  9867  fimaxre2  10109  climcn1  10147  climcn2  10148  subcn2  10150  ndvdssub  10330  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemsup  10398  dfgcd2  10403  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  lcmgcdlem  10459  lcmdvds  10461  coprmgcdb  10470  coprmdvds1  10473  coprmdvds2  10475  prmind2  10502  dvdsprime  10504  nprm  10505  dvdsprm  10518  exprmfct  10519  coprm  10523  isprm6  10526  prmfac1  10531  sqrt2irr  10541  cbvrald  10598  bj-bdfindes  10744  bj-omtrans  10751  bj-inf2vnlem1  10765  bj-inf2vnlem2  10766  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  bj-findes  10776  strcoll2  10778  sscoll2  10783