Theorem imbi1d 612

Description: Deduction adding a consequent to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
imbi1d	⊢ (φ → ((ψ → θ) ↔ (χ → θ)))

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 ⊢ (φ → (ψ ↔ χ))
2	1	negbid 610	. . 3 ⊢ (φ → (¬ ψ ↔ ¬ χ))
3	2	imbi2d 611	. 2 ⊢ (φ → ((¬ θ → ¬ ψ) ↔ (¬ θ → ¬ χ)))
4		pm4.1 164	. 2 ⊢ ((ψ → θ) ↔ (¬ θ → ¬ ψ))
5		pm4.1 164	. 2 ⊢ ((χ → θ) ↔ (¬ θ → ¬ χ))
6	3, 4, 5	3bitr4g 554	1 ⊢ (φ → ((ψ → θ) ↔ (χ → θ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146

This theorem is referenced by:  bibi2d 617  imbi1 622  imbi12d 625  pm5.33 649  con3th 765  drsb1 1174  ax11v2 1214  ax11inda 1370  rgen2a 1697  ralcom2 1774  raleq1f 1781  alexeq 1882  mo2icl 1920  sbcth2 1979  sbc19.21g 1984  ra4sbc 1994  r19.37zv 2348  ssuni 2518  intmin4 2555  trel 2683  ssexg 2717  dtruALT 2744  opth2 2796  pocl 2840  so 2860  onminex 3016  ordunisuc2 3111  dfom2 3129  findsg 3153  tfindsg 3158  tfindsg2 3159  vtoclr 3207  fun11 3558  funimass4 3758  f1fv 3869  caoprcan 4050  oaabs 4245  ertr 4267  ecoptocl 4296  ecopoprtrn 4304  dom2d 4394  unifi 4541  fiint 4543  supmo 4559  supub 4563  suplub 4564  supmaxlem 4571  suppr 4573  supsnALT 4575  karden 4709  aceq1 4712  zorn2lem1 4771  iscard2 4837  axrepndlem2 4928  axregndlem2 4938  indpi 5017  ltsopq 5058  prcdpq 5080  prlem934 5122  supexpr 5146  ltsosr 5186  suppsr 5205  supsrlem6 5213  supsr 5214  supre 5243  ltsor 5244  prodgt0 5785  prodgt0t 5792  prodge0t 5794  lbinfm 6005  infm3 6011  infmsup 6025  xrsupsslem 6033  xrinfmsslem 6034  supxr 6038  primet 6152  raluz 6387  fz1sbct 6462  sqrlem20 6637  abs3lemt 6859  seq1bnd 6862  cau2 6865  cau3i 6866  cau3ir 6867  cau5i 6869  cvg1 6873  cvg3 6875  cvganz 6876  clm3 7032  clm4 7033  climconst 7047  climshft 7057  climaddlem3 7069  climmullem8 7080  caucvglem2 7111  caucvglem5 7114  serzf0 7122  ser1f0 7123  ser1clim0 7126  cvgcmp3cetlem2 7142  cvgcmp3cet 7143  expcnvlem1 7179  expcnvlem6 7184  elcncf1d 7222  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  efaddlem25 7321  islp2 7707  cncnplem3 7736  metcnpi3 7854  metcnpi4 7855  metcni2 7857  cncfmet 7867  lmconst 7896  lmnn 7897  caun0 7907  metcld 7929  metcnp4 7932  xplm 7937  xpcn 7938  iscms2lem4 7954  isnvlem 8193  nvi 8197  nmcnilem 8300  va1cnlem 8307  sm1cnilem 8309  blocni 8424  spwval2 8610  spwpr2 8615  efifolem3 8674  norm3lemt 8974  chlim 9059  hlim0 9060  projlem20 9160  pjth 9188  omlsi 9200  eigortht 9721  0cnop 9860  0cnfn 9861  idcnop 9862  lnopcon 9919  lnfncon 9946  nlelch 9950  stcltr1 10157  elat2 10223  ghomf1olem 10352  fillsb 10494  isded 10585  dedi 10586  iscat 10603  cati 10604  ismona 10651  ismonb 10652  imonclem 10655

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain