Theorem imbi1d 381

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

Hypothesis

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

Assertion

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

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	notbid 356	. . 3 |- (ph -> (-. ps <-> -. ch))
3	2	imbi2d 380	. 2 |- (ph -> ((-. th -> -. ps) <-> (-. th -> -. ch)))
4		con34b 355	. 2 |- ((ps -> th) <-> (-. th -> -. ps))
5		con34b 355	. 2 |- ((ch -> th) <-> (-. th -> -. ch))
6	3, 4, 5	3bitr4g 351	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

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

This theorem is referenced by:  imbi12d 384  imbi1 386  bibi2dOLD 816  pm5.33 1014  con3th 1114  imim21b 1128  drsb1 1848  ax11v2 1890  ax11inda 2055  rgen2a 2441  ralcom2 2521  raleqf 2539  alexeq 2661  mo2icl 2710  sbcth2 2780  sbc19.21g 2786  ra4sbc 2799  csbiebg 2838  r19.37zv 3197  ifeq2 3216  ssuni 3420  intmin4 3459  ssexg 3656  dtru 3694  opth2 3741  pocl 3788  posn 3794  so 3810  eusv2OLD 3995  eusv2 3996  onminex 4063  ordunisuc2 4097  tfinds 4111  tfindsg 4112  tfindsg2 4113  dfom2 4119  findsg 4145  vtoclr 4199  fun11 4619  funimass4 4847  dff13 4984  oprabid 5041  caoprcan 5120  frxp 5250  dfsmo2 5298  oaabs 5510  ertr 5533  errtr 5535  ecoptocl 5566  ecopoprtrn 5574  dom2d 5667  ac6sfi 5718  findcard 5887  findcard2 5888  unifi 5914  fiint 5916  indexfi 5922  supmo 5939  supub 5943  suplub 5944  supmaxlem 5953  suppr 5955  supsnALT 5957  ordtypelem6 5964  karden 6160  iscard2 6196  omsubinit 6246  aceq1 6248  fodomnum 6274  zorn2lem1 6435  iscard2OLD 6495  axrepndlem2 6540  axregndlem2 6550  indpi 6629  ltsopq 6670  prcdpq 6692  prlem934 6734  supexpr 6758  ltsosr 6798  suppsr 6817  supsrlem6 6825  supsr 6826  supre 6855  ltsor 6856  prodgt0i 7430  prodgt0 7437  prodge0 7439  lbinfm 7705  infm3 7711  infmsup 7729  xrsupsslem 7737  xrinfmsslem 7738  supxr 7742  prime 7862  raluz 8072  fz1sbc 8181  sqrlem20 8442  abs3lem 8660  seq1bndi 8663  cau2i 8666  cau3ii 8667  cau3iri 8668  cau5ii 8670  cvg1 8674  cvg3i 8676  cvganz 8677  clm3i 8851  clm4i 8852  climconsti 8866  climshfti 8876  climaddlem3 8888  climmullem8 8899  caucvglem2 8930  caucvglem5 8933  serzf0i 8941  ser1clim0 8945  cvgcmp3cetlem2 8962  cvgcmp3ce 8963  expcnvlem1 9004  expcnvlem6 9009  elcncf1di 9048  ivthlem6 9064  ivthlem7 9065  efaddlem25 9140  rpnnen2 9306  prmdvdsexpb 9520  1arithlem22 9551  1arithlem30 9560  1arithlem31 9561  ispos 9698  lubval 9723  glbval 9728  joinval2 9733  meetval2 9740  islp2 10039  cncnplem3 10069  metcnpi3 10186  metcnpi4 10187  metcni2 10189  cncfmet 10199  lmconst 10228  lmnn 10229  caun0 10239  metcld 10262  metcnp4 10265  metcnp4OLD 10266  xplm 10271  xpcn 10272  iscms2lem4 10288  isnvlem 10582  nvi 10586  vacnlem3 10690  vacnlem4 10691  nmcnilem 10697  va1cnlem 10705  sm1cnilem 10707  blocni 10828  spwval2 11023  spwpr2 11028  efifolem3 11105  fillsb 11266  fbssint 11275  dirtr 11352  unmnd 11401  ringoidmlem 11405  norm3lemt 11646  chlimi 11729  hlim0 11730  projlem20 11830  pjthi 11858  omlsii 11870  eigorth 12391  0cnop 12530  0cnfn 12531  idcnop 12532  lnopconi 12590  lnfnconi 12617  nlelchi 12621  stcltr1i 12835  elat2 12901  bnj1338 13992  bnj1510 14099  bnj1511 14100  bnj1512 14101  bnj1513 14102  bnj517 14188  bnj1145 14360  bnj1154 14367  bnj1171 14368  bnj1172 14369  nqereu 14532  prcdnq 14588  prmdvdsexpbOLD 14602  ghomf1olem 14621  climuzcnv 14632  frxpOLD 14851  poseq 14854  frrlem4 14884  nocvxminlem 14944  dfiota3 15024  alexeqd 15263  cbcpcp 15504  cbicplem 15508  preoref22 15570  supdef 15604  mxlelt2 15606  mxlelt 15607  mnlelt2 15608  dutos1 15626  istoset2 15628  ablcomgrp 15698  intopcoaconlem3b 15922  fbaslim2 15963  exopcopn 15982  isded 16138  dedi 16139  iscat 16156  cati 16157  dualded 16187  dualcat2 16188  ismona 16213  ismonb 16214  imonclem 16217  isepia 16223  isepib 16224  iepiclem 16227  trer 16446  elfiun 16454  finsschain 16458  ordtypelem6OLD 16465  omsubinitOLD 16484  alexsublem4 16525  comppfsc 16602  neibastop2lem3 16606  neibastop2lem4 16607  limfilcf 16672  fmfnfmlem1 16679  fmfnfm 16683  fcluscf 16697  fcluscomplem 16705  findcard2OLD 16830  indexfiOLD 16840  filbcmb 16861  sdc 16896  fdc 16897  fdc1 16898  metdcn 16938  heiborlem16 17055  bfp 17094  divrngidl 17261  pridlval 17266  smprngpr 17285  ertr2 17342  2sbc6g 17464  sbiota1 17484  iscvlat2 17984  isphil 18175  llnexatOLD 18221  psubspset 18449  ldilfset 18742  ldilset 18743  dilfset 18783  dilset 18784  cdlemefrs29bpre0 19066  cdlemefrs29cl 19069  cdlemefrs32fva 19070

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 232

Copyright terms: Public domain