Theorem dedth2h 2387

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

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 612	. . 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 2383	. . 3 |- (ps -> th)
6	2, 5	dedth 2383	. 2 |- (ph -> (ps -> ch))
7	6	imp 350	1 |- ((ph /\ ps) -> ch)

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

This theorem is referenced by:  dedth3h 2388  dedth4h 2389  oawordeu 4189  unfilem3 4550  subclt 5367  negsubt 5382  neg11t 5409  mulneg1t 5451  mul2negt 5454  negdit 5455  addgt0t 5647  addgegt0t 5648  addge0t 5650  ltnegt 5655  lenegt 5657  lesub0t 5678  mulge0t 5679  mul0ort 5696  divclt 5712  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  divrect 5739  divcan3t 5760  divcan3tOLD 5761  rec11 5778  redivclt 5800  prodgt0t 5826  prodge0t 5828  ltrec 5879  ltrect 5884  lerect 5885  lt2msqt 5886  le2msqt 5903  nnsubt 5957  nn0mulclt 6123  snunioo 6415  sq11t 6629  sqeqort 6649  binom2t 6650  sqrmul 6705  sqrlet 6713  sqr2irrlem2 6725  sqr2irrlem5 6728  readdt 6805  imaddt 6808  cjaddt 6812  cjmult 6813  absmult 6858  absdivt 6860  absltt 6880  abslet 6881  cjdivt 6889  abssubt 6894  abstrit 6898  bcpasct 6970  expcnvlem5 7231  efaddt 7367  ef1tlub 7382  ef01tlub 7386  absef01tlub 7388  eirr 7394  reef11t 7409  reefiso 7428  sinaddt 7453  cosaddt 7454  nmlno0 8455  ipassi 8501  sii 8514  ajfun 8521  cosh111t 8717  efif1lem6 8735  hvnegdit 8934  hvsubeq0t 8935  normlem9at 8987  normsub0t 9003  norm-iit 9005  norm-iiit 9007  normsubt 9010  normpytht 9012  norm3adift 9020  normpart 9022  polidt 9026  bcst 9048  occllem2 9174  occllem8 9180  pjtht 9234  axpjpjt 9256  pjoc1t 9267  pjomlt 9269  pjoc2t 9272  shsclt 9282  shslejt 9350  shinclt 9351  chinclt 9422  chsscon3t 9423  chlejb1t 9435  chnlet 9437  chdmm1t 9448  spanunt 9468  elspansn2t 9490  h1datomt 9505  cmbr3t 9551  pjoml2t 9554  pjoml3t 9555  cmcmt 9557  cmcm3t 9558  lecmt 9560  osumt 9588  spansnjt 9592  pjadjt 9630  pjaddt 9631  pjsubt 9633  pjmult 9634  pjcht 9639  pj11t 9659  pjnormt 9669  pjpytht 9670  pjnelt 9671  hosubclt 9699  hoaddcomt 9700  ho0subt 9723  honegsubt 9725  eigret 9761  lnopeq0lem2 9931  lnopeqt 9934  lnopuni 9937  lnophm 9943  cvmdt 10263  chrelat2t 10297  cvexcht 10301  mdsymt 10339  abs2sqlet 10374  abs2sqltt 10375  intprd 10471

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-if 2362

Copyright terms: Public domain