![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bi2anan9 | Structured version Visualization version Unicode version |
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
bi2an9.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bi2an9.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bi2anan9 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2an9.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi1d 712 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | bi2an9.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | anbi2d 711 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | sylan9bb 707 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 |
This theorem is referenced by: bi2anan9r 886 2reu5 3250 ralprg 4023 raltpg 4025 prssg 4130 prsspwg 4132 opelopab2a 4719 opelxp 4867 eqrel 4927 eqrelrel 4939 brcog 5004 tpres 6122 dff13 6164 resoprab2 6398 ovig 6423 dfoprab4f 6856 f1o2ndf1 6909 om00el 7282 oeoe 7305 eroveu 7463 endisj 7664 infxpen 8450 dfac5lem4 8562 sornom 8712 ltsrpr 9506 axcnre 9593 axmulgt0 9713 wloglei 10153 mulge0b 10482 addltmul 10855 ltxr 11422 sumsqeq0 12360 rlim 13571 cpnnen 14293 dvds2lem 14327 gcddvds 14489 opoe 14773 omoe 14774 opeo 14775 omeo 14776 pcqmul 14815 xpsfrnel2 15483 eqgval 16878 frgpuplem 17434 mpfind 18771 2ndcctbss 20482 txbasval 20633 cnmpt12 20694 cnmpt22 20701 prdsxmslem2 21556 ishtpy 22015 bcthlem1 22304 bcth 22309 volun 22510 vitali 22583 itg1addlem3 22668 rolle 22954 mumullem2 24119 lgsquadlem3 24296 lgsquad 24297 2sqlem7 24310 axpasch 24983 usgra2adedgwlkonALT 25356 usgra2wlkspthlem1 25359 el2wlkonotot1 25614 frg2wot1 25797 frg2woteqm 25799 numclwwlkovg 25827 hlimi 26853 leopadd 27797 eqrelrd2 28234 isinftm 28510 metidv 28707 altopthg 30746 altopthbg 30747 brsegle 30887 finxpreclem3 31797 itg2addnclem3 32007 fzadd2 32082 prtlem13 32452 dib1dim 34745 pellex 35691 ssprss 39011 wlkson 39666 |
Copyright terms: Public domain | W3C validator |