Theorem dedth2h 1787

Description: Weak deduction theorem eliminating two hypotheses.

Hypotheses

Ref	Expression
dedth2h.1	⊢ (A = if(φ, A, C) → (χ ↔ θ))
dedth2h.2	⊢ (B = if(ψ, B, D) → (θ ↔ τ))
dedth2h.3	⊢ τ

Assertion

Ref	Expression
dedth2h	⊢ ((φ ∧ ψ) → χ)

Proof of Theorem dedth2h

Step	Hyp	Ref	Expression
1		dedth2h.1	. . . 4 ⊢ (A = if(φ, A, C) → (χ ↔ θ))
2	1	imbi2d 464	. . 3 ⊢ (A = if(φ, A, C) → ((ψ → χ) ↔ (ψ → θ)))
3		dedth2h.2	. . . 4 ⊢ (B = if(ψ, B, D) → (θ ↔ τ))
4		dedth2h.3	. . . 4 ⊢ τ
5	3, 4	dedth 1784	. . 3 ⊢ (ψ → θ)
6	2, 5	dedth 1784	. 2 ⊢ (φ → (ψ → χ))
7	6	imp 277	1 ⊢ ((φ ∧ ψ) → χ)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091  ifcif 1776

This theorem is referenced by:  dedth3h 1788  dedth4h 1789  limsuc 2361  oawordeu 3157  unfilem3 3440  subclt 4140  subnegt 4149  negcon1t 4167  subeq0t 4169  mulneg1t 4196  mul2negt 4199  negdit 4200  mul0ort 4212  divclt 4223  divcan1t 4228  divcan2t 4229  divrect 4238  divcan3t 4251  rec11 4262  redivclt 4276  letrit 4347  addge0t 4362  posdift 4365  ltnegt 4366  lenegt 4368  lesub0t 4374  mulge0t 4375  divgt0t 4402  divge0t 4403  ltrec 4410  ltdiv23 4413  ltrect 4417  lerect 4418  le2sqt 4420  nnsubt 4451  nn0mulclt 4554  sqe11t 4705  lt2sqet 4706  sqrmul 4763  sqr2irrlem2 4778  sqr2irrlem5 4781  cjaddt 4831  cjmult 4832  absmult 4849  absltt 4857  abssubt 4864  hvnegdit 5039  hvsubeq0t 5040  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3adift 5098  occllem2 5181  occllem8 5187  pjtht 5240  axpjpjt 5260  pjoc1t 5270  shsclt 5283  shslejt 5351  shinclt 5352  chinclt 5416  chsscon3t 5417  chlejb1t 5429  chnlet 5431  chdmm1t 5438  elspansn2t 5472  h1datomt 5484  pjoml3t 5517  spansnjt 5540  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcht 5582  pjnormt 5666  pjnelt 5667  chrelat2t 5761  cvexcht 5763

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-if 1777

metamath.org