Theorem dedth2h 3015

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

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298  ifcif 2982

This theorem is referenced by:  dedth3h 3016  dedth4h 3017  dedth2v 3018  oawordeu 5237  oeoa 5272  unfilem3 5643  subcl 6524  negsub 6540  neg11 6569  mulneg1 6615  mul2negOLD 6619  negdi 6620  addgt0OLD 6832  addgegt0OLD 6834  addge0OLD 6838  ltneg 6844  leneg 6846  lesub0 6867  mulge0 6868  mulge0OLD 6869  mul0or 6884  divcl 6901  divcan1 6909  divrec 6922  divcan3 6938  rec11i 6954  redivcl 6978  prodgt0 7004  prodge0 7006  ltreci 7062  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  nnsub 7141  nn0mulcl 7332  snunioo 7584  sq11 7874  sqeqor 7895  binom2 7896  sqrmuli 7955  sqrle 7963  sqr2irrlem2 7975  sqr2irrlem5 7978  readd 8055  imadd 8058  cjadd 8062  cjmul 8063  absmul 8109  absdiv 8111  abslt 8132  absle 8133  cjdiv 8141  abssub 8146  abstri 8150  bcpasc 8222  expcnvlem5 8492  efadd 8629  ef1tlubi 8644  ef01tlubi 8648  absef01tlubi 8650  eirr 8656  reef11 8674  reefiso 8693  sinadd 8718  cosadd 8719  nmlno0 9795  ipassi 9842  sii 9855  ajfun 9862  cosh111 10071  efif1lem6 10089  hvnegdi 10566  hvsubeq0 10567  normlem9at 10620  normsub0 10636  norm-ii 10638  norm-iii 10640  normsub 10643  normpyth 10645  norm3adifi 10653  normpar 10655  polid 10659  bcs 10681  occllem2 10807  occllem8 10813  pjth 10867  axpjpj 10889  pjoc1 10900  pjoml 10902  pjoc2 10905  shscl 10915  shslej 10983  shincl 10984  chincl 11055  chsscon3 11056  chlejb1 11068  chnle 11070  chdmm1 11081  spanun 11101  elspansn2 11123  h1datom 11138  cmbr3 11184  pjoml2 11187  pjoml3 11188  cmcm 11190  cmcm3 11191  lecm 11193  osum 11223  spansnj 11227  pjadji 11265  pjaddi 11266  pjsubi 11268  pjmuli 11269  pjch 11274  pj11 11294  pjnorm 11304  pjpyth 11305  pjnel 11306  hosubcl 11336  hoaddcom 11337  ho0sub 11360  honegsub 11362  eigre 11398  lnopeq0lem2 11568  lnopeq 11571  lnopunii 11574  lnophmi 11580  cvmd 11908  chrelat2 11942  cvexch 11946  mdsym 11984  fz1eqb 13609  abs2sqle 13624  abs2sqlt 13625  divalglem7 13702  divalg 13706  infxpg 14422  subsp2 14902  erthdmg 15730  add20 15777  eluzadd 15782  eluzsub 15783  txcnoprab 15911  bfp 16009

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