Theorem breq12i 3347

Description: Equality inference for a binary relation. (The proof was shortened by Eric Schmidt, 4-Apr-2007.)

Hypotheses

Ref	Expression
breq1i.1	|- A = B
breq12i.2	|- C = D

Assertion

Ref	Expression
breq12i	|- (ARC <-> BRD)

Proof of Theorem breq12i

Step	Hyp	Ref	Expression
1		breq1i.1	. 2 |- A = B
2		breq12i.2	. 2 |- C = D
3		breq12 3343	. 2 |- ((A = B /\ C = D) -> (ARC <-> BRD))
4	1, 2, 3	mp2an 761	1 |- (ARC <-> BRD)

Syntax hints:   <-> wb 163   = wceq 1298   class class class wbr 3338

This theorem is referenced by:  3brtr3g 3368  3brtr4g 3369  caoprord2 4990  ltsopq 6227  ltapq 6228  ltmpq 6229  ltaddpq 6231  prlem936a 6305  ltsosr 6355  ltasr 6361  ltpsrpr 6371  ltadd1i 6766  leadd2i 6768  ltnegi 6783  lesub0iOLD 6793  ltdiv1ii 7001  ltrecii 7061  halfposi 7087  lt2sqi 7869  le2sqi 7870  discrlem1 7906  nn0le2msqi 7913  sqrlem16 7938  inelr 7985  reefiso 8693  ruclem2 8780  ruclem15 8793  pjthlem1 10852  mdsldmd1i 11903

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-9 1307  ax-10 1308  ax-11 1309  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-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339

Copyright terms: Public domain