Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  th3qlem2 Unicode version

Theorem th3qlem2 6651
 Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypotheses
Ref Expression
th3q.1
th3q.2
th3q.4
Assertion
Ref Expression
th3qlem2
Distinct variable groups:   ,,,,,,,,,   ,,,,,,,,,   ,,,,,,,   ,,,,,,,   , ,,,,,,,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem th3qlem2
StepHypRef Expression
1 th3q.2 . . 3
2 eqid 2253 . . . . 5
3 breq1 3923 . . . . . . . 8
43anbi1d 688 . . . . . . 7
5 oveq1 5717 . . . . . . . 8
65breq1d 3930 . . . . . . 7
74, 6imbi12d 313 . . . . . 6
87imbi2d 309 . . . . 5
9 breq2 3924 . . . . . . . 8
109anbi1d 688 . . . . . . 7
11 oveq1 5717 . . . . . . . 8
1211breq2d 3932 . . . . . . 7
1310, 12imbi12d 313 . . . . . 6
1413imbi2d 309 . . . . 5
15 breq1 3923 . . . . . . . . . 10
1615anbi2d 687 . . . . . . . . 9
17 oveq2 5718 . . . . . . . . . 10
1817breq1d 3930 . . . . . . . . 9
1916, 18imbi12d 313 . . . . . . . 8
2019imbi2d 309 . . . . . . 7
21 breq2 3924 . . . . . . . . . 10
2221anbi2d 687 . . . . . . . . 9
23 oveq2 5718 . . . . . . . . . 10
2423breq2d 3932 . . . . . . . . 9
2522, 24imbi12d 313 . . . . . . . 8
2625imbi2d 309 . . . . . . 7
27 th3q.4 . . . . . . . 8
2827expcom 426 . . . . . . 7
292, 20, 26, 282optocl 4672 . . . . . 6
3029com12 29 . . . . 5
312, 8, 14, 302optocl 4672 . . . 4
3231imp 420 . . 3
331, 32th3qlem1 6650 . 2
34 opex 4130 . . . . . 6
35 opex 4130 . . . . . 6
36 eceq1 6582 . . . . . . . . 9
3736eqeq2d 2264 . . . . . . . 8
38 eceq1 6582 . . . . . . . . 9
3938eqeq2d 2264 . . . . . . . 8
4037, 39bi2anan9 848 . . . . . . 7
41 oveq12 5719 . . . . . . . . 9
42 eceq1 6582 . . . . . . . . 9
4341, 42syl 17 . . . . . . . 8
4443eqeq2d 2264 . . . . . . 7
4540, 44anbi12d 694 . . . . . 6
4634, 35, 45cla42ev 2813 . . . . 5
4746exlimivv 2025 . . . 4
4847exlimivv 2025 . . 3
4948immoi 2160 . 2
5033, 49syl 17 1
 Colors of variables: wff set class Syntax hints:   wi 6   wa 360  wex 1537   wceq 1619   wcel 1621  wmo 2115  cvv 2727  cop 3547   class class class wbr 3920   cxp 4578  (class class class)co 5710   wer 6543  cec 6544  cqs 6545 This theorem is referenced by:  th3qcor  6652  th3q  6653 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713  df-er 6546  df-ec 6548  df-qs 6552
 Copyright terms: Public domain W3C validator