Theorem imbi1d 616

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

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	notbid 614	. . 3 |- (ph -> (-. ps <-> -. ch))
3	2	imbi2d 615	. 2 |- (ph -> ((-. th -> -. ps) <-> (-. th -> -. ch)))
4		con34b 164	. 2 |- ((ps -> th) <-> (-. th -> -. ps))
5		con34b 164	. 2 |- ((ch -> th) <-> (-. th -> -. ch))
6	3, 4, 5	3bitr4g 558	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144

This theorem is referenced by:  bibi2d 621  imbi1 626  imbi12d 629  pm5.33 653  con3th 771  drsb1 1212  ax11v2 1252  ax11inda 1410  rgen2a 1745  ralcom2 1822  raleq1f 1829  alexeq 1931  mo2icl 1969  sbcth2 2030  sbc19.21g 2035  ra4sbc 2047  r19.37zv 2405  ssuni 2589  intmin4 2626  trel 2761  ssexg 2795  el 2822  dtru 2831  opth2 2876  pocl 2922  posn 2928  so 2943  onminex 3164  ordunisuc2 3198  tfindsg 3213  tfindsg2 3214  dfom2 3220  findsg 3245  vtoclr 3294  fun11 3667  funimass4 3874  dff13 3988  caoprcan 4116  oaabs 4392  ertr 4414  ecoptocl 4444  ecopoprtrn 4452  dom2d 4545  ac6sfi 4591  unifi 4701  fiint 4703  supmo 4719  supub 4723  suplub 4724  supmaxlem 4731  suppr 4733  supsnALT 4735  karden 4872  aceq1 4875  zorn2lem1 4934  iscard2 5004  axrepndlem2 5099  axregndlem2 5109  indpi 5188  ltsopq 5229  prcdpq 5251  prlem934 5293  supexpr 5317  ltsosr 5357  suppsr 5376  supsrlem6 5384  supsr 5385  supre 5414  ltsor 5415  prodgt0i 5959  prodgt0 5966  prodge0 5968  lbinfm 6216  infm3 6222  infmsup 6236  xrsupsslem 6244  xrinfmsslem 6245  supxr 6249  prime 6366  raluz 6569  fz1sbc 6648  sqrlem20 6893  abs3lem 7110  seq1bndi 7113  cau2i 7116  cau3ii 7117  cau3iri 7118  cau5ii 7120  cvg1 7124  cvg3i 7126  cvganz 7127  clm3i 7282  clm4i 7283  climconsti 7297  climshfti 7307  climaddlem3 7319  climmullem8 7330  caucvglem2 7361  caucvglem5 7364  serzf0i 7372  ser1clim0 7376  cvgcmp3cetlem2 7393  cvgcmp3ce 7394  expcnvlem1 7431  expcnvlem6 7436  elcncf1di 7475  ivthlem6 7491  ivthlem7 7492  efaddlem25 7567  islp2 7957  cncnplem3 7986  metcnpi3 8103  metcnpi4 8104  metcni2 8106  cncfmet 8116  lmconst 8145  lmnn 8146  caun0 8156  metcld 8178  metcnp4 8181  xplm 8186  xpcn 8187  iscms2lem4 8203  isnvlem 8476  nvi 8480  vacnlem3 8584  vacnlem4 8585  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  blocni 8720  spwval2 8915  spwpr2 8920  efifolem3 8996  norm3lemt 9295  chlimi 9380  hlim0 9381  projlem20 9481  pjthi 9509  omlsii 9521  eigorth 10044  0cnop 10182  0cnfn 10183  idcnop 10184  lnopconi 10242  lnfnconi 10269  nlelchi 10273  stcltr1i 10482  elat2 10548  ghomf1olem 10681  unmnd 10951  uridm 10956  fillsb 11073  isded 11190  dedi 11191  iscat 11208  cati 11209  ismona 11264  ismonb 11265  imonclem 11268  isepia 11274  isepib 11275  iepiclem 11278  trer 11409  elfiun 11421  finsschain 11425  ordtypelem6 11432  omsubinit 11451  alexsublem4 11499  comppfsc 11578  neibastop2lem3 11582  neibastop2lem4 11583  fbssint 11626  limfilcf 11683  fmfnfmlem1 11700  fmfnfm 11704  fcluscf 11724  fcluscomplem 11732  dirtr 11753  findcard 11836  indexf 11847  filbcmb 11857  sdc 11877  metdcn 11918  heiborlem16 12026  bfp 12065

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 145  df-an 223

Copyright terms: Public domain