Theorem equncomi 3649

Description: Inference form of equncom 3648. equncomi 3649 was automatically derived from equncomiVD 33669 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)

Hypothesis

Ref	Expression
equncomi.1

Assertion

Ref	Expression
equncomi

Proof of Theorem equncomi

Step	Hyp	Ref	Expression
1		equncomi.1	. 2
2		equncom 3648	. 2
3	1, 2	mpbi 208	1

Syntax hints:  =wceq 1395  u.cun 3473

This theorem is referenced by:  disjssun  3884  difprsn1  4166  unidmrn  5542  phplem1  7716  ackbij1lem14  8634  ltxrlt  9676  ruclem6  13968  ruclem7  13969  i1f1  22097  subfacp1lem1  28623  pwfi2f1o  31044  usgfislem1  32444  usgfisALTlem1  32448  sucidALTVD  33670  sucidALT  33671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480