Theorem dedth 3011

Description: Weak deduction theorem that eliminates a hypothesis ph, making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B. The hypothesis ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 3021. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 3027 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.

Hypotheses

Ref	Expression
dedth.1	|- (A = if(ph, A, B) -> (ps <-> ch))
dedth.2	|- ch

Assertion

Ref	Expression
dedth	|- (ph -> ps)

Proof of Theorem dedth

Step	Hyp	Ref	Expression
1		dedth.2	. 2 |- ch
2		iftrue 2989	. . . 4 |- (ph -> if(ph, A, B) = A)
3	2	eqcomd 1889	. . 3 |- (ph -> A = if(ph, A, B))
4		dedth.1	. . 3 |- (A = if(ph, A, B) -> (ps <-> ch))
5	3, 4	syl 12	. 2 |- (ph -> (ps <-> ch))
6	1, 5	mpbiri 211	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  ifcif 2982

This theorem is referenced by:  dedth2h 3015  dedth3h 3016  orduninsuc 3925  rdgsuc 5153  rdglim 5156  oeoe 5274  limensuc 5601  supsr 6383  negneg 6553  subid 6555  subid1 6556  renegcl 6600  mul01 6606  msqgt0 6797  msqge0 6798  gt0ne0 6800  mulcan 6880  divmulzi 6895  divclzi 6900  divcan1zi 6907  divcan2zi 6908  recne0zi 6914  recne0 6915  recid 6918  divreczi 6921  divdirzi 6932  divcan3zi 6936  div1 6949  recrec 6952  redivcli 6976  redivclzi 6977  eqneg 6983  prodgt0i 6997  ltmul1i 7000  ltdiv1i 7002  2times 7188  halfpos 7222  nneo 7410  peano5uzti 7416  sqge0 7878  discrlem2 7907  sqrlem6 7928  sqrlem12 7934  sqrlem20 7942  sqrlem21 7943  sqrlem22 7944  sqrthi 7949  sqrcli 7950  sqrgt0i 7951  sqrcl 7960  sqrgt0 7961  sqrge0 7962  sqr00 7964  sqrsq 7972  sqsqr 7973  cjreb 8050  cjmulrcl 8051  cjmulval 8052  cjmulge0 8053  reneg 8054  imneg 8057  cjcj 8061  cjneg 8064  addcj 8065  absval2 8103  abs00 8104  absge0 8105  absid 8113  absgt0 8145  abslem2 8161  clm4a 8350  clmi2a 8351  climconst3 8356  iserzshft2i 8367  serzclim0 8369  climubi 8414  caucvg3 8428  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  cvgcmp3ce 8451  expcnvlem3 8490  geolim 8499  geolim1 8501  cvgratlem2ALT 8510  efseq1ex 8568  reefcl 8580  efcj 8599  efaddlem24 8623  eftlex 8640  ef4p 8665  efgt0 8670  eflegeo 8681  efm1legeo 8683  reeff1olem2 8690  ruclem25 8803  ruclem29 8807  ruclem32 8810  ruclem33 8811  ruclem35 8813  ruclem37 8815  ruclem39 8817  methaus 9160  bcth 9310  grpidval 9342  addinv 9436  imsmet 9656  vacnlem4 9670  vacn 9673  nmcn 9678  nmlno0i 9794  nmblolbi 9800  blocn 9807  ipdir 9843  ipass 9846  siilem2 9853  ubthi 9889  efifolem1 10076  erdisj2 10164  dif1card 10177  ac6sg 10188  issubsplem1 10246  issubspt 10247  fora2 10407  normlem6 10614  normlem7tALT 10618  normsq 10634  hlimcauii 10739  hlimcaui 10740  hhssabl 10766  hhssnvt 10768  hhsssh 10772  occl 10815  projlem1 10819  projlem16 10834  projlem17 10835  projlem28 10846  projlem29 10847  pjthlem8 10859  pjthlem9 10860  pjthlem14 10865  pjthi 10866  pjtheu 10869  ococ 10881  shintcl 10927  chintcl 10929  chm0 11047  chne0 11050  chocin 11051  chj0 11053  chjo 11071  h1de2ci 11112  spansn 11115  elspansn 11122  pjch1 11250  pjinormi 11267  pjige0 11271  hoaddid1 11354  hodid 11355  hmopbdoptHIL 11550  nmlnop0 11560  lnopunilem2 11573  elunop2 11575  lnophm 11581  nmbdoplb 11587  nmcopex 11596  nmcoplb 11597  lnopcon 11601  lnfn0 11613  lnfnmul 11614  nmbdfnlb 11616  nmcfnex 11625  nmcfnlb 11626  lnfncon 11628  riesz4 11634  riesz1 11635  cnlnadjeu 11648  pjhmop 11721  hmopidmch 11725  hmopidmpj 11726  pjss2coi 11736  pjssmi 11737  pjssge0i 11738  pjdifnormi 11739  pjidmco 11753  mdslmd1lem3 11899  mdslmd1lem4 11900  csmdsymi 11906  hatomic 11932  atord 11960  atcvat2 11961  irred 11967  bnj147 12480  bnj148 12481  bnj209OLD 12501  bnj210OLD 12503  bnj211OLD 12505  bnj519 12520  bnj941 12842  bnj517 13259  bnj939 13338  fndmeng 13598  cayleythlem 13645  moec 14351  ac5g 14388  snelpwg 14415  pw2eng 14419  infsdomnng 14423  prnzg 14454  fprod1s1 14679  fprodp1s1 14683  fprod1i2 14685  distopg 14876  homindlem3 14900  subspemp2 14904  clindistop2 14963  topgrpsubcn 14982  ishomd 15139  topmtcl 15525  fimaxg 15747  supclt 15762  supubt 15763  supeut 15767  fsumltisumi 15823  fsumleisumi 15826  bfplem11 16008  reparpht 16065

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-if 2983

Copyright terms: Public domain