Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Theorem hbabd 2162
 Description: Deduction form of bound-variable hypothesis builder hbab 2161.
Hypotheses
Ref Expression
hbabd.1
hbabd.2
Assertion
Ref Expression
hbabd
Distinct variable group:   ,

Proof of Theorem hbabd
StepHypRef Expression
1 hbabd.1 . . . . 5
2 ax-7 1621 . . . . 5
31, 2syl 13 . . . 4
4 hbabd.2 . . . . 5
542alimi 1657 . . . 4
6 hbsb4t 1925 . . . 4
73, 5, 63syl 38 . . 3
8 ax-16 1883 . . 3
97, 8pm2.61d2 205 . 2
10 df-clab 2158 . 2
1110albii 1664 . 2
129, 10, 113imtr4g 333 1
 Colors of variables: wff set class Syntax hints:   wn 2   wi 3  wal 1613   wceq 1615   wcel 1617  wsbc 1843  cab 2157 This theorem is referenced by:  hbcsb1g 2830  hbcsbg 2832  hbifd 3229  hbiotad 5263 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-10 1625  ax-12 1627  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893 This theorem depends on definitions:  df-bi 232  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158
Copyright terms: Public domain