Theorem dedth2h 2383

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 2380 but requires that each hypothesis has exactly one class variable. See also comments in dedth 2379.

Hypotheses

Ref	Expression
dedth2h.1	|- (A = if(ph, A, C) -> (ch <-> th))
dedth2h.2	|- (B = if(ps, B, D) -> (th <-> ta))
dedth2h.3	|- ta

Assertion

Ref	Expression
dedth2h	|- ((ph /\ ps) -> ch)

Proof of Theorem dedth2h

Step	Hyp	Ref	Expression
1		dedth2h.1	. . . 4 |- (A = if(ph, A, C) -> (ch <-> th))
2	1	imbi2d 611	. . 3 |- (A = if(ph, A, C) -> ((ps -> ch) <-> (ps -> th)))
3		dedth2h.2	. . . 4 |- (B = if(ps, B, D) -> (th <-> ta))
4		dedth2h.3	. . . 4 |- ta
5	3, 4	dedth 2379	. . 3 |- (ps -> th)
6	2, 5	dedth 2379	. 2 |- (ph -> (ps -> ch))
7	6	imp 350	1 |- ((ph /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954  ifcif 2357

This theorem is referenced by:  dedth3h 2384  dedth4h 2385  oawordeu 4179  unfilem3 4532  subclt 5347  negsubt 5362  neg11t 5389  mulneg1t 5431  mul2negt 5434  negdit 5435  addgt0t 5628  addgegt0t 5629  addge0t 5631  ltnegt 5636  lenegt 5638  lesub0t 5659  mulge0t 5660  mul0ort 5673  divclt 5689  divcan1t 5697  divcan2t 5698  divrect 5710  divcan3t 5726  rec11 5742  redivclt 5764  prodgt0t 5790  prodge0t 5792  ltrec 5835  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  nnsubt 5912  nn0mulclt 6078  snunioo 6356  sq11t 6568  sqeqort 6588  binom2t 6589  sqrmul 6643  sqrlet 6651  sqr2irrlem2 6663  sqr2irrlem5 6666  readdt 6748  imaddt 6751  cjaddt 6755  cjmult 6756  absmult 6801  absdivt 6803  absltt 6825  abslttOLD 6826  abslet 6827  cjdivt 6835  abssubt 6840  abstrit 6843  bcpasct 6916  expcnvlem5 7174  efaddt 7317  ef1tlub 7332  ef01tlub 7335  absef01tlub 7337  eirr 7343  reeff1 7358  reefiso 7378  sinaddt 7403  cosaddt 7404  nmlno0 8400  ipassi 8445  sii 8458  ajfun 8465  cosh111t 8651  efif1lem6 8669  hvnegdit 8873  hvsubeq0t 8874  normlem9at 8926  normsub0t 8942  norm-iit 8944  norm-iiit 8946  normsubt 8949  normpytht 8951  norm3adift 8959  normpart 8961  polidt 8965  bcst 8987  occllem2 9113  occllem8 9119  pjtht 9172  axpjpjt 9194  pjoc1t 9205  pjomlt 9207  pjoc2t 9210  shsclt 9220  shslejt 9288  shinclt 9289  chinclt 9360  chsscon3t 9361  chlejb1t 9373  chnlet 9375  chdmm1t 9386  spanunt 9406  elspansn2t 9429  h1datomt 9445  cmbr3t 9491  pjoml2t 9494  pjoml3t 9495  cmcmt 9497  cmcm3t 9498  lecmt 9500  osumt 9528  spansnjt 9532  pjadjt 9570  pjaddt 9571  pjsubt 9573  pjmult 9574  pjcht 9579  pj11t 9599  pjnormt 9609  pjpytht 9610  pjnelt 9611  hosubclt 9639  hoaddcomt 9640  ho0subt 9663  honegsubt 9665  eigret 9701  lnopeq0lem2 9869  lnopeqt 9872  lnopuni 9875  lnophm 9881  cvmdt 10200  chrelat2t 10234  cvexcht 10238  mdsymt 10276  abs2sqlet 10308  abs2sqltt 10309  intprd 10403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-if 2358

Copyright terms: Public domain